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: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) by WSIERP_1:2 ;
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