defpred S₁[ Nat] means for G being Group
for a, b being Element of G holds (a |^ $1) |^ b = (a |^ b) |^ $1;
A1: S₁[ 0 ] by Lm2;
A2: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm3;
for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; :: thesis: verum