let n be Nat; :: thesis: (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2)
defpred S₁[ Nat] means (tau_bar to_power $1) + (tau_bar to_power ($1 + 1)) = tau_bar to_power ($1 + 2);
A1: S₁[ 0 ]

proof

(tau_bar to_power 0 ) + (tau_bar to_power (0 + 1)) = 1 + (tau_bar to_power 1) by POWER:29
.= 1 + ((1 - (sqrt 5)) / 2) by FIB_NUM:def 2, POWER:30
.= (((1 - (sqrt 5)) - (sqrt 5)) + 5) / 4
.= (((1 - (sqrt 5)) - (sqrt 5)) + (sqrt (5 ^2 ))) / 4 by SQUARE_1:89
.= (((1 - (1 * (sqrt 5))) - ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 by SQUARE_1:97
.= 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 (0 + 2) ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: tau_bar + 1 = tau_bar + (tau_bar to_power 0 ) by POWER:29
.= tau_bar to_power 2 by A1, POWER:30 ;
A3: S₁[1]

proof

(tau_bar to_power 1) + (tau_bar to_power (1 + 1)) = tau_bar + (tau_bar to_power (1 + 1)) by POWER:30
.= tau_bar + ((tau_bar to_power 1) * (tau_bar to_power 1)) by FIB_NUM2:7
.= tau_bar + ((tau_bar to_power 1) * tau_bar ) by POWER:30
.= tau_bar + (tau_bar * tau_bar ) by POWER:30
.= tau_bar * (1 + tau_bar )
.= (tau_bar to_power 1) * (tau_bar to_power 2) by A2, POWER:30
.= tau_bar to_power (1 + 2) by FIB_NUM2:7 ;
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
S₁[k] and
S₁[k + 1] ; :: thesis: S₁[k + 2]
(tau_bar to_power (k + 2)) + (tau_bar to_power ((k + 2) + 1)) = (tau_bar to_power (k + 2)) + ((tau_bar to_power (k + 2)) * (tau_bar to_power 1)) by FIB_NUM2:7
.= (tau_bar to_power (k + 2)) * (1 + (tau_bar to_power 1))
.= (tau_bar to_power (k + 2)) * (tau_bar to_power 2) by A2, POWER:30
.= tau_bar to_power ((k + 2) + 2) by FIB_NUM2:7 ;
hence S₁[k + 2] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from FIB_NUM:sch 1(A1, A3, A4);
hence (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2) ; :: thesis: verum