let E be set ; :: thesis: for A being Subset of (E ^omega )
for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ k,l) = A |^.. (n + k)
let A be Subset of (E ^omega ); :: 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) ^^ (A |^ k,l) c= A |^.. (n + k)

proof

let x be set ; :: 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
A3: ( a in A |^.. n & b in A |^ k,l & 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 A3, FLANG_1:def 1;
hence x in A |^.. (n + k) by A3, Th18; :: thesis: verum

end;

A |^.. (n + k) c= (A |^.. n) ^^ (A |^ k,l)

proof

let x be set ; :: 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
A4: ( i >= n + k & x in A |^ i ) by Th2;
consider m being Nat such that
A5: (n + k) + m = i by A4, NAT_1:10;
i = (n + m) + k by A5;
then x in (A |^ (n + m)) ^^ (A |^ k) by A4, FLANG_1:34;
then consider a, b being Element of E ^omega such that
A6: ( a in A |^ (n + m) & b in A |^ k & x = a ^ b ) by FLANG_1:def 1;
A7: A |^ k c= A |^ k,l by A1, FLANG_2:20;
A |^ (n + m) c= A |^.. n by Th3, NAT_1:11;
hence x in (A |^.. n) ^^ (A |^ k,l) by A6, A7, FLANG_1:def 1; :: thesis: verum

end;

hence (A |^.. n) ^^ (A |^ k,l) = A |^.. (n + k) by A2, XBOOLE_0:def 10; :: thesis: verum