let i be Nat; :: thesis: for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let S be 1-sorted ; :: thesis: for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let F be Function of S,S; :: thesis: for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let s1, s2 be Element of S; :: thesis: for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let n, m be Nat; :: thesis: ( (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 implies (F |^ (m + (i * n))) . s1 = s2 )
assume that
A1: (F |^ m) . s1 = s2 and
A2: (F |^ n) . s2 = s2 ; :: thesis: (F |^ (m + (i * n))) . s1 = s2
defpred S₁[ Nat] means (F |^ (m + ($1 * n))) . s1 = s2;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: dom (F |^ (m + (i * n))) = the carrier of S by FUNCT_2:52;

per cases ( the carrier of S <> {} or the carrier of S = {} ) ;

suppose A6: the carrier of S <> {} ; :: thesis: S₁[i + 1]

thus (F |^ (m + ((i + 1) * n))) . s1 = (F |^ (n + (m + (i * n)))) . s1
.= ((F |^ n) * (F |^ (m + (i * n)))) . s1 by Th20
.= s2 by A2, A4, A5, A6, FUNCT_1:13 ; :: thesis: verum

end;

suppose the carrier of S = {} ; :: thesis: S₁[i + 1]

then ( not s1 in dom (F |^ (m + ((i + 1) * n))) & s2 = {} ) by SUBSET_1:def 1;
hence (F |^ (m + ((i + 1) * n))) . s1 = s2 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

A7: S₁[ 0 ] by A1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A3);
hence (F |^ (m + (i * n))) . s1 = s2 ; :: thesis: verum