let k be Nat; :: thesis: (@' 1) |^ k = k
defpred S₁[ Nat] means (@' 1) |^ $1 = $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume (@' 1) |^ k = k ; :: thesis: S₁[k + 1]
then ((@' 1) |^ k) * (@' 1) = k + 1 ;
hence S₁[k + 1] by GROUP_1:34; :: thesis: verum

end;

A2: S₁[ 0 ] by Th13, GROUP_1:25;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence (@' 1) |^ k = k ; :: thesis: verum