let n be Nat; :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for x being Element of L holds <%x%> `^ n = <%(x |^ n)%>
let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for x being Element of L holds <%x%> `^ n = <%(x |^ n)%>
let x be Element of L; :: thesis: <%x%> `^ n = <%(x |^ n)%>
set X = <%x%>;
defpred S<sub>1</sub>[ Nat] means <%x%> `^ $1 = <%(x |^ $1)%>;
A1: S₁[ 0 ]

proof

A2: <%(x |^ 0)%> = <%(1_ L)%> by BINOM:8;
1_. L = <%(1_ L)%>

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (1_. L) . n = <%(1_ L)%> . n

per cases ( n = 0 or n >= 1 ) by NAT_1:14;

suppose n = 0 ; :: thesis: (1_. L) . n = <%(1_ L)%> . n

then ( <%(1_ L)%> . n = 1_ L & (1_. L) . n = 1. L ) by POLYNOM5:32, POLYNOM3:30;
hence (1_. L) . n = <%(1_ L)%> . n ; :: thesis: verum

end;

suppose n >= 1 ; :: thesis: (1_. L) . n = <%(1_ L)%> . n

then ( <%(1_ L)%> . n = 0. L & (1_. L) . n = 0. L ) by POLYNOM5:32, POLYNOM3:30;
hence (1_. L) . n = <%(1_ L)%> . n ; :: thesis: verum

end;

end;

end;

hence S₁[ 0 ] by POLYNOM5:15, A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: <%x%> `^ (n + 1) = (<%x%> `^ n) *' <%x%> by POLYNOM5:19;
let k be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k

per cases ( k = 0 or k >= 1 ) by NAT_1:14;

suppose k = 0 ; :: thesis: (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k

then A6: ( (<%x%> `^ n) . k = x |^ n & <%(x |^ (n + 1))%> . k = x |^ (n + 1) & x |^ 1 = x ) by A4, POLYNOM5:32, BINOM:8;
then (<%x%> `^ (n + 1)) . k = (x |^ n) * (x |^ 1) by A5, Th7;
hence (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k by A6, BINOM:10; :: thesis: verum

end;

suppose A7: k >= 1 ; :: thesis: (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k

then (<%x%> `^ n) . k = 0. L by A4, POLYNOM5:32;
then (<%x%> `^ (n + 1)) . k = (0. L) * x by A5, Th7;
hence (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k by A7, POLYNOM5:32; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence <%x%> `^ n = <%(x |^ n)%> ; :: thesis: verum