defpred S₁[ Nat] means (Lucas ($1 + 3)) * (Lucas $1) = ((Lucas ($1 + 2)) |^ 2) - ((Lucas ($1 + 1)) |^ 2);
A1: 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
S₁[k] and
S₁[k + 1] ; :: thesis: S₁[k + 2]
(Lucas ((k + 2) + 3)) * (Lucas (k + 2)) = (Lucas ((k + 3) + 2)) * (Lucas (k + 2))
.= ((Lucas (k + 3)) + (Lucas ((k + 3) + 1))) * (Lucas (k + 2)) by Th12
.= ((Lucas (k + 3)) + (Lucas ((k + 2) + 2))) * (Lucas (k + 2))
.= ((Lucas (k + 3)) + ((Lucas (k + 2)) + (Lucas ((k + 2) + 1)))) * (Lucas (k + 2)) by Th12
.= (((Lucas (k + 2)) + (Lucas (k + 3))) * ((Lucas (k + 2)) + (Lucas ((k + 2) + 1)))) - ((Lucas (k + 3)) * (Lucas (k + 3)))
.= (((Lucas (k + 2)) + (Lucas (k + 3))) * (Lucas ((k + 2) + 2))) - ((Lucas (k + 3)) * (Lucas (k + 3))) by Th12
.= (((Lucas (k + 2)) + (Lucas ((k + 2) + 1))) * (Lucas (k + 4))) - ((Lucas (k + 3)) * (Lucas (k + 3)))
.= ((Lucas ((k + 2) + 2)) * (Lucas (k + 4))) - ((Lucas (k + 3)) * (Lucas (k + 3))) by Th12
.= ((Lucas (k + 4)) * (Lucas (k + 4))) - ((Lucas (k + 3)) |^ 2) by WSIERP_1:1
.= ((Lucas ((k + 2) + 2)) |^ 2) - ((Lucas ((k + 2) + 1)) |^ 2) by WSIERP_1:1 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(Lucas (1 + 3)) * (Lucas 1) = (4 * 4) - (3 * 3) by Th11, Th16
.= (4 * 4) - (3 |^ 2) by WSIERP_1:1
.= ((Lucas (1 + 2)) |^ 2) - ((Lucas (1 + 1)) |^ 2) by Th14, Th15, WSIERP_1:1 ;
then A2: S₁[1] ;
((Lucas (0 + 2)) |^ 2) - ((Lucas (0 + 1)) |^ 2) = (3 * 3) - ((Lucas 1) |^ 2) by Th14, WSIERP_1:1
.= 9 - (1 * 1) by Th11, WSIERP_1:1
.= (Lucas (0 + 3)) * (Lucas 0) by Th11, Th15 ;
then A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A3, A2, A1);
hence for n being Element of NAT holds (Lucas (n + 3)) * (Lucas n) = ((Lucas (n + 2)) |^ 2) - ((Lucas (n + 1)) |^ 2) ; :: thesis: verum