let a, b, k, n be Element of NAT ; :: thesis: GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n))
defpred S₁[ Nat] means GenFib ((k * a),(k * b),$1) = k * (GenFib (a,b,$1));
A1: for i being Nat st S₁[i] & S₁[i + 1] holds
S₁[i + 2]

proof

let i be Nat; :: thesis: ( S₁[i] & S₁[i + 1] implies S₁[i + 2] )
assume that
A2: S₁[i] and
A3: S₁[i + 1] ; :: thesis: S₁[i + 2]
GenFib ((k * a),(k * b),(i + 2)) = (k * (GenFib (a,b,i))) + (GenFib ((k * a),(k * b),(i + 1))) by A2, Th34
.= k * ((GenFib (a,b,i)) + (GenFib (a,b,(i + 1)))) by A3
.= k * (GenFib (a,b,(i + 2))) by Th34 ;
hence S₁[i + 2] ; :: thesis: verum

end;

GenFib ((k * a),(k * b),1) = k * b by Th32
.= k * (GenFib (a,b,1)) by Th32 ;
then A4: S₁[1] ;
GenFib ((k * a),(k * b),0) = k * a by Th32
.= k * (GenFib (a,b,0)) by Th32 ;
then A5: S₁[ 0 ] ;
for i being Nat holds S₁[i] from FIB_NUM:sch 1(A5, A4, A1);
hence GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n)) ; :: thesis: verum