let E be set ; :: thesis: for A being Subset of ()
for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)

let A be Subset of (); :: thesis: for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)

let k, l, n be Nat; :: thesis: ( k <= l implies (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) )
assume A1: k <= l ; :: thesis: (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
A2: A |^.. (n + k) c= (A |^.. n) ^^ (A |^ (k,l))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. (n + k) or x in (A |^.. n) ^^ (A |^ (k,l)) )
assume x in A |^.. (n + k) ; :: thesis: x in (A |^.. n) ^^ (A |^ (k,l))
then consider i being Nat such that
A3: i >= n + k and
A4: x in A |^ i by Th2;
consider m being Nat such that
A5: (n + k) + m = i by ;
i = (n + m) + k by A5;
then x in (A |^ (n + m)) ^^ (A |^ k) by ;
then A6: ex a, b being Element of E ^omega st
( a in A |^ (n + m) & b in A |^ k & x = a ^ b ) by FLANG_1:def 1;
A7: A |^ (n + m) c= A |^.. n by ;
A |^ k c= A |^ (k,l) by ;
hence x in (A |^.. n) ^^ (A |^ (k,l)) by ; :: thesis: verum
end;
(A |^.. n) ^^ (A |^ (k,l)) c= A |^.. (n + k)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^.. n) ^^ (A |^ (k,l)) or x in A |^.. (n + k) )
assume x in (A |^.. n) ^^ (A |^ (k,l)) ; :: thesis: x in A |^.. (n + k)
then consider a, b being Element of E ^omega such that
A8: a in A |^.. n and
A9: b in A |^ (k,l) and
A10: x = a ^ b by FLANG_1:def 1;
A |^ (k,l) c= A |^.. k by Th6;
then a ^ b in (A |^.. n) ^^ (A |^.. k) by ;
hence x in A |^.. (n + k) by ; :: thesis: verum
end;
hence (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) by ; :: thesis: verum