let f, g be sequence of [:COMPLEX,COMPLEX:]; :: thesis: ( f . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds f . (n + 1) = [((((f . n) `1) ^2) + (D * (((f . n) `2) ^2))),((2 * ((f . n) `1)) * ((f . n) `2))] ) & g . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds g . (n + 1) = [((((g . n) `1) ^2) + (D * (((g . n) `2) ^2))),((2 * ((g . n) `1)) * ((g . n) `2))] ) implies f = g )
assume that
A2: f . 0 = [((2 * (m ^2)) + 1),(2 * m)] and
A3: for n being Nat holds f . (n + 1) = [((((f . n) `1) ^2) + (D * (((f . n) `2) ^2))),((2 * ((f . n) `1)) * ((f . n) `2))] and
A4: g . 0 = [((2 * (m ^2)) + 1),(2 * m)] and
A5: for n being Nat holds g . (n + 1) = [((((g . n) `1) ^2) + (D * (((g . n) `2) ^2))),((2 * ((g . n) `1)) * ((g . n) `2))] ; :: thesis: f = g
defpred S₁[ Nat] means f . $1 = g . $1;
A6: S₁[ 0 ] by A2, A4;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus f . (k + 1) = [((((f . k) `1) ^2) + (D * (((f . k) `2) ^2))),((2 * ((f . k) `1)) * ((f . k) `2))] by A3
.= g . (k + 1) by A5, A8 ; :: thesis: verum

end;

A9: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A7);
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: f . n = g . n
thus f . n = g . n by A9; :: thesis: verum