(x : lpFiniteModes ℕ) (n : ℕ) : (((ann (ann x) : lpFiniteModes ℕ) : L2I ℕ) : ℕ → ℂ) n = (Real.sqrt ((n : ℝ) + 1) : ℂ) * (Real.sqrt ((n : ℝ) + 2) : ℂ) * ((x : L2I ℕ) : ℕ → ℂ) (n + 2)

Initializing...

(x : lpFiniteModes ℕ) (n : ℕ) : (((ann (ann x) : lpFiniteModes ℕ) : L2I ℕ) : ℕ → ℂ) n = (Real.sqrt ((n : ℝ) + 1) : ℂ) * (Real.sqrt ((n : ℝ) + 2) : ℂ) * ((x : L2I ℕ) : ℕ → ℂ) (n + 2) · Prove2Me