let n be 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₁[ Nat] means Product ($1 |-> a) = a |^ $1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1] by Lm2;
A2: S₁[ 0 ] by Lm1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence Product (n |-> a) = a |^ n ; :: thesis: verum