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 + 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 A3, NAT_1:10;
i = (n + m) + k by A5;
then x in (A |^ (n + m)) ^^ (A |^ k) by A4, FLANG_1:33;
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 Th3, NAT_1:11;
A |^ k c= A |^ (k,l) by A1, FLANG_2:20;
hence x in (A |^.. n) ^^ (A |^ (k,l)) by A6, A7, FLANG_1:def 1; :: 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 A8, A9, FLANG_1:def 1;
hence x in A |^.. (n + k) by A10, Th18; :: thesis: verum

end;

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