let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
let m, n be Nat; :: thesis: (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
defpred S₁[ Nat] means (A |^.. m) ^^ (A |^.. $1) = A |^.. (m + $1);

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(A |^.. m) ^^ (A |^.. (n + 1)) = (A |^.. m) ^^ ((A |^.. n) ^^ A) by Th16
.= (A |^.. (m + n)) ^^ A by A2, FLANG_1:18
.= A |^.. ((m + n) + 1) by Th16 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(A |^.. m) ^^ (A |^.. 0) = (A |^.. m) ^^ (A *) by Th11
.= A |^.. (m + 0) by Th17 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) ; :: thesis: verum