let L be non empty 1-sorted ; :: thesis: for f being Function of L,L
for n, m being Nat holds f `^ (n * m) = (f `^ n) `^ m
let f be Function of L,L; :: thesis: for n, m being Nat holds f `^ (n * m) = (f `^ n) `^ m
let n, m be Nat; :: thesis: f `^ (n * m) = (f `^ n) `^ m
defpred S<sub>1</sub>[ Nat] means f `^ (n * $1) = (f `^ n) `^ $1;
f `^ (n * 0) = id L by T1
.= (f `^ n) `^ 0 by T1 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
f `^ (n * (k + 1)) = f `^ ((n * k) + n)
.= ((f `^ n) `^ k) * (f `^ n) by IV, lemf
.= (f `^ n) `^ (k + 1) by T3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence f `^ (n * m) = (f `^ n) `^ m ; :: thesis: verum