let a, b, n be Element of NAT ; :: thesis: GenFib a,b,n = ((((a * (- tau_bar )) + b) * (tau to_power n)) + (((a * tau ) - b) * (tau_bar to_power n))) / (sqrt 5)
defpred S₁[ Nat] means GenFib a,b,$1 = ((((a * (- tau_bar )) + b) * (tau to_power $1)) + (((a * tau ) - b) * (tau_bar to_power $1))) / (sqrt 5);
((((a * (- tau_bar )) + b) * (tau to_power 1)) + (((a * tau ) - b) * (tau_bar to_power 1))) / (sqrt 5) = ((((a * (- tau_bar )) + b) * tau ) + (((a * tau ) - b) * (tau_bar to_power 1))) / (sqrt 5) by POWER:30
.= ((((a * (- tau_bar )) + b) * tau ) + (((a * tau ) - b) * tau_bar )) / (sqrt 5) by POWER:30
.= (b * (tau - tau_bar )) / (sqrt 5)
.= b by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:90
.= GenFib a,b,1 by Th32 ;
then A1: S₁[1] ;
A2: 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] )
set c = tau to_power k;
set d = tau_bar to_power k;
A3: tau to_power (k + 1) = (tau to_power k) * (tau to_power 1) by POWER:32
.= (tau to_power k) * tau by POWER:30 ;
set g = (((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k));
A4: tau_bar to_power (k + 1) = (tau_bar to_power k) * (tau_bar to_power 1) by FIB_NUM2:7
.= (tau_bar to_power k) * tau_bar by POWER:30 ;
(sqrt 5) * (sqrt 5) = 5 by Th2;
then A5: 1 + tau = ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (2 * 2) by FIB_NUM:def 1
.= tau * tau by FIB_NUM:def 1
.= (tau to_power 1) * tau by POWER:30
.= (tau to_power 1) * (tau to_power 1) by POWER:30
.= tau to_power (1 + 1) by POWER:32 ;
A6: 1 + tau_bar = (((1 - (sqrt 5)) - (sqrt 5)) + 5) / 4 by FIB_NUM:def 2
.= (((1 - (1 * (sqrt 5))) - ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 by Th2
.= tau_bar * tau_bar by FIB_NUM:def 2
.= (tau_bar to_power 1) * tau_bar by POWER:30
.= (tau_bar to_power 1) * (tau_bar to_power 1) by POWER:30
.= tau_bar to_power (1 + 1) by FIB_NUM2:7
.= tau_bar to_power 2 ;
set h = ((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar );
A7: ( tau to_power (k + 2) = (tau to_power k) * (tau to_power 2) & tau_bar to_power (k + 2) = (tau_bar to_power k) * (tau_bar to_power 2) ) by FIB_NUM2:7;
assume ( S₁[k] & S₁[k + 1] ) ; :: thesis: S₁[k + 2]
then GenFib a,b,(k + 2) = (((((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k))) / (sqrt 5)) + ((((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar )) / (sqrt 5)) by A3, A4, Th34
.= (((((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k))) + (((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar ))) / (sqrt 5) by XCMPLX_1:63
.= ((((a * (- tau_bar )) + b) * (tau to_power (k + 2))) + (((a * tau ) - b) * (tau_bar to_power (k + 2)))) / (sqrt 5) by A7, A5, A6 ;
hence S₁[k + 2] ; :: thesis: verum

end;

((((a * (- tau_bar )) + b) * (tau to_power 0 )) + (((a * tau ) - b) * (tau_bar to_power 0 ))) / (sqrt 5) = ((((a * (- tau_bar )) + b) * 1) + (((a * tau ) - b) * (tau_bar to_power 0 ))) / (sqrt 5) by POWER:29
.= (((a * (- tau_bar )) + b) + (((a * tau ) - b) * 1)) / (sqrt 5) by POWER:29
.= (a * (tau - tau_bar )) / (sqrt 5)
.= a by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:90
.= GenFib a,b,0 by Th32 ;
then A8: S₁[ 0 ] ;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A8, A1, A2);
hence GenFib a,b,n = ((((a * (- tau_bar )) + b) * (tau to_power n)) + (((a * tau ) - b) * (tau_bar to_power n))) / (sqrt 5) ; :: thesis: verum