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:25
.= ((((a * (- tau_bar)) + b) * tau) + (((a * tau) - b) * tau_bar)) / (sqrt 5) by POWER:25
.= (b * (tau - tau_bar)) / (sqrt 5)
.= b by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:89
.= 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:27
.= (tau to_power k) * tau by POWER:25 ;
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:5
.= (tau_bar to_power k) * tau_bar by POWER:25 ;
(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:25
.= (tau to_power 1) * (tau to_power 1) by POWER:25
.= tau to_power (1 + 1) by POWER:27 ;
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:25
.= (tau_bar to_power 1) * (tau_bar to_power 1) by POWER:25
.= tau_bar to_power (1 + 1) by FIB_NUM2:5
.= 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:5;
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:62
.= ((((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:24
.= (((a * (- tau_bar)) + b) + (((a * tau) - b) * 1)) / (sqrt 5) by POWER:24
.= (a * (tau - tau_bar)) / (sqrt 5)
.= a by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:89
.= 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