let a, b, k, n be Element of NAT ; :: thesis: GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n))

defpred S_{1}[ Nat] means GenFib ((k * a),(k * b),$1) = k * (GenFib (a,b,$1));

A1: for i being Nat st S_{1}[i] & S_{1}[i + 1] holds

S_{1}[i + 2]

.= k * (GenFib (a,b,1)) by Th32 ;

then A4: S_{1}[1]
;

GenFib ((k * a),(k * b),0) = k * a by Th32

.= k * (GenFib (a,b,0)) by Th32 ;

then A5: S_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from FIB_NUM:sch 1(A5, A4, A1);

hence GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n)) ; :: thesis: verum

defpred S

A1: for i being Nat st S

S

proof

GenFib ((k * a),(k * b),1) =
k * b
by Th32
let i be Nat; :: thesis: ( S_{1}[i] & S_{1}[i + 1] implies S_{1}[i + 2] )

assume that

A2: S_{1}[i]
and

A3: S_{1}[i + 1]
; :: thesis: S_{1}[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_{1}[i + 2]
; :: thesis: verum

end;assume that

A2: S

A3: S

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

.= k * (GenFib (a,b,1)) by Th32 ;

then A4: S

GenFib ((k * a),(k * b),0) = k * a by Th32

.= k * (GenFib (a,b,0)) by Th32 ;

then A5: S

for i being Nat holds S

hence GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n)) ; :: thesis: verum