let n be Element of NAT ; :: thesis: for G being Group
for a being Element of G holds Product (n |-> a) = a |^ n
let G be Group; :: thesis: for a being Element of G holds Product (n |-> a) = a |^ n
let a be Element of G; :: thesis: Product (n |-> a) = a |^ n
defpred S₁[ Element of NAT ] means Product ($1 |-> a) = a |^ $1;
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1] by Lm2;
A2: S₁[ 0 ] by Lm1;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1);
hence Product (n |-> a) = a |^ n ; :: thesis: verum