let f, g be [:COMPLEX,COMPLEX:] -valued ManySortedSet of NAT ; :: thesis: ( f . 0 = [a,b] & ( for n being Nat holds f . (n + 1) = [(((x1 * ((f . n) `1)) + (x2 * ((f . n) `2))) + x3),(((y1 * ((f . n) `1)) + (y2 * ((f . n) `2))) + y3)] ) & g . 0 = [a,b] & ( for n being Nat holds g . (n + 1) = [(((x1 * ((g . n) `1)) + (x2 * ((g . n) `2))) + x3),(((y1 * ((g . n) `1)) + (y2 * ((g . n) `2))) + y3)] ) implies f = g )
assume that
A3: f . 0 = [a,b] and
A4: for n being Nat holds f . (n + 1) = [(((x1 * ((f . n) `1)) + (x2 * ((f . n) `2))) + x3),(((y1 * ((f . n) `1)) + (y2 * ((f . n) `2))) + y3)] and
A5: g . 0 = [a,b] and
A6: for n being Nat holds g . (n + 1) = [(((x1 * ((g . n) `1)) + (x2 * ((g . n) `2))) + x3),(((y1 * ((g . n) `1)) + (y2 * ((g . n) `2))) + y3)] ; :: thesis: f = g
defpred S₁[ Nat] means f . $1 = g . $1;
A7: S₁[ 0 ] by A3, A5;
A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
thus f . (n + 1) = [(((x1 * ((f . n) `1)) + (x2 * ((f . n) `2))) + x3),(((y1 * ((f . n) `1)) + (y2 * ((f . n) `2))) + y3)] by A4
.= g . (n + 1) by A6, A9 ; :: thesis: verum

end;

A10: for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A8);
let n be object ; :: according to PBOOLE:def 21 :: thesis: ( n is set & n is Element of NAT implies f . n = g . n )
thus ( n is set & n is Element of NAT implies f . n = g . n ) by A10; :: thesis: verum