defpred S₁[ Nat] means Fib $1 = ((tau to_power $1) - (tau_bar to_power $1)) / (sqrt 5);
A1: S₁[ 0 ]

proof

tau_bar to_power 0 = 1 by POWER:29;
then ((tau to_power 0 ) - (tau_bar to_power 0 )) / (sqrt 5) = (1 - 1) / (sqrt 5) by POWER:29
.= 0 ;
hence S₁[ 0 ] by PRE_FF:1; :: thesis: verum

end;

A2: S₁[1]

proof

A3: tau - tau_bar = sqrt 5 ;
tau_bar to_power 1 = tau_bar by POWER:30;
then ((tau to_power 1) - (tau_bar to_power 1)) / (sqrt 5) = (sqrt 5) / (sqrt 5) by A3, POWER:30
.= Fib 1 by Lm10, PRE_FF:1, XCMPLX_1:60 ;
hence S₁[1] ; :: thesis: verum

end;

A4: 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] )
assume that
A5: S₁[k] and
A6: S₁[k + 1] ; :: thesis: S₁[k + 2]
set a = tau to_power k;
set a1 = tau_bar to_power k;
set b = tau to_power (k + 1);
set b1 = tau_bar to_power (k + 1);
set c = tau to_power (k + 2);
set c1 = tau_bar to_power (k + 2);
A7: tau to_power (k + 2) = (tau to_power 2) * (tau to_power k) by Lm12, POWER:32
.= (tau to_power k) * (tau + 1) by Lm8, POWER:53
.= ((tau to_power k) * tau ) + ((tau to_power k) * 1)
.= ((tau to_power k) * (tau to_power 1)) + (tau to_power k) by POWER:30
.= (tau to_power k) + (tau to_power (k + 1)) by Lm12, POWER:32 ;
tau_bar to_power (k + 2) = tau_bar |^ (k + 2) by POWER:46
.= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:13
.= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:11
.= (tau_bar |^ k) * (tau_bar + 1) by Lm8, NEWTON:10
.= ((tau_bar |^ k) * tau_bar ) + ((tau_bar |^ k) * 1)
.= (tau_bar |^ (k + 1)) + ((tau_bar |^ k) * 1) by NEWTON:11
.= (tau_bar to_power (k + 1)) + (tau_bar |^ k) by POWER:46
.= (tau_bar to_power k) + (tau_bar to_power (k + 1)) by POWER:46 ;
then A8: ((tau to_power k) - (tau_bar to_power k)) + ((tau to_power (k + 1)) - (tau_bar to_power (k + 1))) = (tau to_power (k + 2)) - (tau_bar to_power (k + 2)) by A7;
Fib (k + 2) = Fib ((k + 1) + 1)
.= (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) + (((tau to_power (k + 1)) - (tau_bar to_power (k + 1))) / (sqrt 5)) by A5, A6, PRE_FF:1
.= ((tau to_power (k + 2)) - (tau_bar to_power (k + 2))) / (sqrt 5) by A8, XCMPLX_1:63 ;
hence S₁[k + 2] ; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from FIB_NUM:sch 1(A1, A2, A4); :: thesis: verum