let n be Nat; :: thesis: for R being commutative Ring holds
( (<%(0. R),(0. R),(1_ R)%> `^ n) . (2 * n) = 1_ R & ( for k being Nat st k <> 2 * n holds
(<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R ) )
let R be commutative Ring; :: thesis: ( (<%(0. R),(0. R),(1_ R)%> `^ n) . (2 * n) = 1_ R & ( for k being Nat st k <> 2 * n holds
(<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R ) )
set x1 = <%(0. R),(1_ R)%>;
set x2 = <%(0. R),(0. R),(1_ R)%>;
set 2n = 2 * n;
defpred S₁[ Nat] means <%(0. R),(0. R),(1_ R)%> `^ $1 = <%(0. R),(1_ R)%> `^ (2 * $1);
( <%(0. R),(0. R),(1_ R)%> `^ 0 = 1_. R & 1_. R = <%(0. R),(1_ R)%> `^ 0 ) by POLYNOM5:15;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A3: <%(0. R),(0. R),(1_ R)%> = <%(0. R),(1_ R)%> `^ 2 by Th6
.= <%(0. R),(1_ R)%> *' <%(0. R),(1_ R)%> by POLYNOM5:17 ;
assume S<sub>1</sub>[k] ; :: thesis: S<sub>1</sub>[k + 1]
hence <%(0. R),(0. R),(1_ R)%> `^ (k + 1) = (<%(0. R),(1_ R)%> `^ (2 * k)) *' <%(0. R),(0. R),(1_ R)%> by POLYNOM5:19
.= ((<%(0. R),(1_ R)%> `^ (2 * k)) *' <%(0. R),(1_ R)%>) *' <%(0. R),(1_ R)%> by A3, POLYNOM3:33
.= (<%(0. R),(1_ R)%> `^ ((2 * k) + 1)) *' <%(0. R),(1_ R)%> by POLYNOM5:19
.= <%(0. R),(1_ R)%> `^ (((2 * k) + 1) + 1) by POLYNOM5:19
.= <%(0. R),(1_ R)%> `^ (2 * (k + 1)) ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
then A4: <%(0. R),(0. R),(1_ R)%> `^ n = <%(0. R),(1_ R)%> `^ (2 * n) ;
defpred S₂[ Nat] means (1_ R) |^ $1 = 1_ R;
A5: S₂[ 0 ] by BINOM:8;
A6: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
hence (1_ R) |^ (k + 1) = (1_ R) * (1_ R) by GROUP_1:def 7
.= 1_ R ;
:: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A5, A6);
then A7: S₂[2 * n] ;
( n = 0 or n > 0 ) ;
hence (<%(0. R),(0. R),(1_ R)%> `^ n) . (2 * n) = 1_ R by A4, Th9, A7; :: thesis: for k being Nat st k <> 2 * n holds
(<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R
let k be Nat; :: thesis: ( k <> 2 * n implies (<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R )
thus ( k <> 2 * n implies (<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R ) by A4, Th9; :: thesis: verum