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) * (f `^ m)
let f be Function of L,L; :: thesis: for n, m being Nat holds f `^ (n + m) = (f `^ n) * (f `^ m)
let n, m be Nat; :: thesis: f `^ (n + m) = (f `^ n) * (f `^ m)
defpred S<sub>1</sub>[ Nat] means f `^ (n + $1) = (f `^ n) * (f `^ $1);
f `^ (n + 0) = (f `^ n) * (id L)
.= (f `^ n) * (f `^ 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) + 1)
.= ((f `^ n) * (f `^ k)) * f by IV, T3
.= (f `^ n) * ((f `^ k) * f) by T2
.= (f `^ n) * (f `^ (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) * (f `^ m) ; :: thesis: verum