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