defpred S₁[ Nat, Element of [:COMPLEX,COMPLEX:], Element of [:COMPLEX,COMPLEX:]] means $3 = [((($2 `1) ^2) + (D * (($2 `2) ^2))),((2 * ($2 `1)) * ($2 `2))];
A1: for n being Nat
for x being Element of [:COMPLEX,COMPLEX:] ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of [:COMPLEX,COMPLEX:] ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]
let x be Element of [:COMPLEX,COMPLEX:]; :: thesis: ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]
take In ([(In ((((x `1) ^2) + (D * ((x `2) ^2))),COMPLEX)),(In (((2 * (x `1)) * (x `2)),COMPLEX))],[:COMPLEX,COMPLEX:]) ; :: thesis: S₁[n,x, In ([(In ((((x `1) ^2) + (D * ((x `2) ^2))),COMPLEX)),(In (((2 * (x `1)) * (x `2)),COMPLEX))],[:COMPLEX,COMPLEX:])]
thus S₁[n,x, In ([(In ((((x `1) ^2) + (D * ((x `2) ^2))),COMPLEX)),(In (((2 * (x `1)) * (x `2)),COMPLEX))],[:COMPLEX,COMPLEX:])] ; :: thesis: verum

end;

ex f being sequence of [:COMPLEX,COMPLEX:] st
( f . 0 = In ([(In (((2 * (m ^2)) + 1),COMPLEX)),(In ((2 * m),COMPLEX))],[:COMPLEX,COMPLEX:]) & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
hence ex b₁ being sequence of [:COMPLEX,COMPLEX:] st
( b₁ . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds b₁ . (n + 1) = [((((b₁ . n) `1) ^2) + (D * (((b<sub>1</sub> . n) `2) ^2))),((2 * ((b₁ . n) `1)) * ((b<sub>1</sub> . n) `2))] ) ) ; :: thesis: verum