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))

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

(A |^.. n) ^^ (A |^ (k,l)) c= A |^.. (n + k)
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;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

proof

hence
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
by A2, XBOOLE_0:def 10; :: thesis: verum
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;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