let M be non empty multMagma ; :: thesis: for a being Element of M
for n being Nat holds (power M) . (a,n) is Element of M
let a be Element of M; :: thesis: for n being Nat holds (power M) . (a,n) is Element of M
defpred S₁[ Nat] means (power M) . (a,$1) is Element of M;
(power M) . (a,0) = 1_ M by GROUP_1:def 7;
then P0: S₁[ 0 ] ;

P1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider b = (power M) . (a,n) as Element of M ;
n - 0 is Element of NAT by NAT_1:21;
then (power M) . (a,(n + 1)) = b * a by GROUP_1:def 7;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
hence for n being Nat holds (power M) . (a,n) is Element of M ; :: thesis: verum