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 S1[ Nat] means <%x%> `^ \$1 = <%(x |^ \$1)%>;
A1: S1[ 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 ;
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 ;
hence (1_. L) . n = <%(1_ L)%> . n ; :: thesis: verum
end;
end;
end;
hence S1[ 0 ] by ; :: thesis: verum
end;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A4: S1[n] ; :: thesis: S1[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 ;
then (<%x%> `^ (n + 1)) . k = (x |^ n) * (x |^ 1) by ;
hence (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k by ; :: thesis: verum
end;
suppose A7: k >= 1 ; :: thesis: (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k
then (<%x%> `^ n) . k = 0. L by ;
then (<%x%> `^ (n + 1)) . k = (0. L) * x by ;
hence (<%x%> `^ (n + 1)) . k = <%(x |^ (n + 1))%> . k by ; :: thesis: verum
end;
end;
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A3);
hence <%x%> `^ n = <%(x |^ n)%> ; :: thesis: verum