let a, b be Element of NAT ; :: thesis: GenFib (a,a,b) = ((GenFib (a,a,0)) / 2) * ((Fib b) + (Lucas b))
defpred S₁[ Nat] means GenFib (a,a,$1) = ((GenFib (a,a,0)) / 2) * ((Fib $1) + (Lucas $1));
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
A2: S₁[k] and
A3: S₁[k + 1] ; :: thesis: S₁[k + 2]
GenFib (a,a,(k + 2)) = (((GenFib (a,a,0)) / 2) * ((Fib k) + (Lucas k))) + (GenFib (a,a,(k + 1))) by A2, Th34
.= ((GenFib (a,a,0)) / 2) * (((Fib k) + (Fib (k + 1))) + ((Lucas k) + (Lucas (k + 1)))) by A3
.= ((GenFib (a,a,0)) / 2) * ((Fib (k + 2)) + ((Lucas k) + (Lucas (k + 1)))) by FIB_NUM2:24
.= ((GenFib (a,a,0)) / 2) * ((Fib (k + 2)) + (Lucas (k + 2))) by Th12 ;
hence S₁[k + 2] ; :: thesis: verum

end;

GenFib (a,a,1) = a by Th32;
then A4: S₁[1] by Th11, Th32, PRE_FF:1;
A5: S₁[ 0 ] by Th11, PRE_FF:1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A5, A4, A1);
hence GenFib (a,a,b) = ((GenFib (a,a,0)) / 2) * ((Fib b) + (Lucas b)) ; :: thesis: verum