let a, b be Element of NAT ; :: thesis: for k being Nat holds ((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = (((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)
let k be Nat; :: thesis: ((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = (((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)
set a1 = GenFib (a,b,(k + 1));
set b1 = GenFib (a,b,((k + 1) + 1));
((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = ((((GenFib (a,b,(k + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 1))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,(k + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1)))) by Th5
.= (((GenFib (a,b,(k + 1))) * (GenFib (a,b,(k + 1)))) + (2 * ((GenFib (a,b,(k + 1))) * (GenFib (a,b,((k + 1) + 1)))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1))))
.= (((GenFib (a,b,(k + 1))) |^ 2) + ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1)))) by WSIERP_1:1
.= (((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 WSIERP_1:1 ;
hence ((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = (((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) ; :: thesis: verum