let a, b, n be Element of NAT ; :: thesis: ((GenFib a,b,(n + 2)) * (GenFib a,b,n)) - ((GenFib a,b,(n + 1)) |^ 2) = ((- 1) to_power n) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3)))
defpred S₁[ Nat] means ((GenFib a,b,($1 + 2)) * (GenFib a,b,$1)) - ((GenFib a,b,($1 + 1)) |^ 2) = ((- 1) to_power $1) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3)));
A1: GenFib a,b,2 = GenFib a,b,(0 + 2)
.= (GenFib a,b,0 ) + (GenFib a,b,(0 + 1)) by Th34
.= a + (GenFib a,b,1) by Th32
.= a + b by Th32 ;
A2: GenFib a,b,3 = GenFib a,b,(1 + 2)
.= (GenFib a,b,1) + (GenFib a,b,(1 + 1)) by Th32
.= b + (a + b) by A1, Th32
.= (2 * b) + a ;
A3: S₁[ 0 ]

proof

((GenFib a,b,(0 + 2)) * (GenFib a,b,0 )) - ((GenFib a,b,(0 + 1)) |^ 2) = ((GenFib a,b,2) * a) - ((GenFib a,b,1) |^ 2) by Th32
.= ((a + b) * a) - (b |^ 2) by A1, Th32
.= ((a * a) + (b * a)) - (b * b) by WSIERP_1:2
.= ((a + b) * (a + b)) - (b * ((2 * b) + a))
.= 1 * (((GenFib a,b,2) |^ 2) - (b * (GenFib a,b,3))) by A1, A2, WSIERP_1:2
.= ((- 1) to_power 0 ) * (((GenFib a,b,2) |^ 2) - (b * (GenFib a,b,3))) by POWER:29
.= ((- 1) to_power 0 ) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by Th32 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A4: S₁[1]

proof

((GenFib a,b,(1 + 2)) * (GenFib a,b,1)) - ((GenFib a,b,(1 + 1)) |^ 2) = (((2 * b) + a) * b) - ((a + b) |^ 2) by A1, A2, Th32
.= (((2 * b) * b) + (a * b)) - ((a + b) * (a + b)) by WSIERP_1:2
.= (- 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a)))
.= ((- 1) to_power 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a))) by POWER:30
.= ((- 1) to_power 1) * (((a + b) |^ 2) - (b * (GenFib a,b,3))) by A2, WSIERP_1:2
.= ((- 1) to_power 1) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by A1, Th32 ;
hence S₁[1] ; :: thesis: verum

end;

A5: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A6: S₁[k] and
A7: S₁[k + 1] ; :: thesis: S₁[k + 2]
set c = (GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1));
set d = (GenFib a,b,(k + 2)) * (GenFib a,b,k);
(GenFib a,b,2) |^ 2 = (GenFib a,b,(0 + 2)) |^ 2
.= ((GenFib a,b,0 ) + (GenFib a,b,(0 + 1))) |^ 2 by Th34
.= (a + (GenFib a,b,1)) |^ 2 by Th32
.= (a + b) |^ 2 by Th32 ;
then A8: ((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3)) = ((a + b) |^ 2) - (b * (GenFib a,b,(1 + 2))) by Th32
.= ((a + b) |^ 2) - (b * ((GenFib a,b,1) + (GenFib a,b,(1 + 1)))) by Th34
.= ((a + b) |^ 2) - (b * (b + (GenFib a,b,(0 + 2)))) by Th32
.= ((a + b) |^ 2) - (b * (b + ((GenFib a,b,0 ) + (GenFib a,b,(0 + 1))))) by Th34
.= ((a + b) |^ 2) - (b * (b + (a + (GenFib a,b,1)))) by Th32
.= ((a + b) |^ 2) - (b * (b + (a + b))) by Th32
.= ((((a + b) |^ 2) - (b * b)) - (b * a)) - (b * b)
.= ((((((a * a) + (a * b)) + (b * a)) + (b * b)) - (b * b)) - (b * a)) - (b * b) by Th5
.= ((a * a) + (a * b)) - (b * b) ;
A9: ((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1))) - ((GenFib a,b,((k + 1) + 1)) |^ 2) = ((- 1) to_power (k + 1)) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by A7;
A10: ((- 1) to_power (k + 1)) + ((- 1) to_power k) = (((- 1) to_power k) * ((- 1) to_power 1)) + ((- 1) to_power k) by FIB_NUM2:7
.= (((- 1) to_power k) * (- 1)) + ((- 1) to_power k) by POWER:30
.= 0 ;
((GenFib a,b,(k + 2)) * (GenFib a,b,k)) - ((GenFib a,b,(k + 1)) |^ 2) = ((- 1) to_power k) * (((a * a) + (a * b)) - (b * b)) by A6, A8;
then A11: (((- 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + (((GenFib a,b,(k + 2)) * (GenFib a,b,k)) - ((GenFib a,b,(k + 1)) |^ 2)) = (((- 1) to_power (k + 1)) + ((- 1) to_power k)) * (((a * a) + (a * b)) - (b * b))
.= (((a * a) + (a * b)) - (b * b)) * 0 by A10 ;
A12: (((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - (((GenFib a,b,(k + 1)) + (GenFib a,b,((k + 1) + 1))) |^ 2) = (((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - ((((GenFib a,b,(k + 1)) |^ 2) + ((2 * (GenFib a,b,(k + 1))) * (GenFib a,b,((k + 1) + 1)))) + ((GenFib a,b,((k + 1) + 1)) |^ 2)) by Th33
.= (((((- 1) to_power (k + 1)) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3)))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - ((GenFib a,b,(k + 1)) |^ 2)) - ((2 * (GenFib a,b,(k + 1))) * (GenFib a,b,((k + 1) + 1))) by A9
.= (((((- 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - ((GenFib a,b,(k + 1)) |^ 2)) - ((2 * (GenFib a,b,(k + 1))) * (GenFib a,b,((k + 1) + 1))) by A8
.= - ((2 * (GenFib a,b,(k + 1))) * (GenFib a,b,((k + 1) + 1))) by A11 ;
((GenFib a,b,((k + 2) + 2)) * (GenFib a,b,(k + 2))) - ((GenFib a,b,((k + 2) + 1)) |^ 2) = (((GenFib a,b,(k + 2)) + (GenFib a,b,((k + 2) + 1))) * (GenFib a,b,(k + 2))) - ((GenFib a,b,((k + 2) + 1)) |^ 2) by Th34
.= (((GenFib a,b,((k + 2) + 1)) + (GenFib a,b,(k + 2))) * ((GenFib a,b,k) + (GenFib a,b,(k + 1)))) - ((GenFib a,b,((k + 1) + 2)) |^ 2) by Th34
.= (((((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,k)) + ((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1)))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,(k + 1)))) - (((GenFib a,b,(k + 1)) + (GenFib a,b,((k + 1) + 1))) |^ 2) by Th32
.= (((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,k)) + ((GenFib a,b,(k + 2)) * (GenFib a,b,(k + 1)))) + ((((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,(k + 1))) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - (((GenFib a,b,(k + 1)) + (GenFib a,b,((k + 1) + 1))) |^ 2))
.= (((GenFib a,b,((k + 2) + 1)) * (GenFib a,b,k)) + ((GenFib a,b,(k + 2)) * (GenFib a,b,(k + 1)))) + (- ((2 * (GenFib a,b,(k + 1))) * (GenFib a,b,(k + 2)))) by A12
.= ((GenFib a,b,((k + 1) + 2)) * (GenFib a,b,k)) - ((GenFib a,b,(k + 2)) * (GenFib a,b,(k + 1)))
.= (((GenFib a,b,(k + 1)) + (GenFib a,b,((k + 1) + 1))) * (GenFib a,b,k)) - ((GenFib a,b,(k + 2)) * (GenFib a,b,(k + 1))) by Th34
.= (((GenFib a,b,(k + 1)) * (GenFib a,b,k)) + ((GenFib a,b,(k + 2)) * (GenFib a,b,k))) - (((GenFib a,b,k) + (GenFib a,b,(k + 1))) * (GenFib a,b,(k + 1))) by Th34
.= ((GenFib a,b,(k + 2)) * (GenFib a,b,k)) - ((GenFib a,b,(k + 1)) * (GenFib a,b,(k + 1)))
.= (((- 1) to_power k) * 1) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by A6, WSIERP_1:2
.= (((- 1) to_power k) * (1 to_power 2)) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by POWER:31
.= (((- 1) to_power k) * ((- 1) to_power 2)) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by Th3
.= ((- 1) to_power (k + 2)) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) by FIB_NUM2:7 ;
hence S₁[k + 2] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from FIB_NUM:sch 1(A3, A4, A5);
hence ((GenFib a,b,(n + 2)) * (GenFib a,b,n)) - ((GenFib a,b,(n + 1)) |^ 2) = ((- 1) to_power n) * (((GenFib a,b,2) |^ 2) - ((GenFib a,b,1) * (GenFib a,b,3))) ; :: thesis: verum