let E be set ; 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); for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
let k, l, n be Nat; ( k <= l implies (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) )
assume A1:
k <= l
; (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
A2:
A |^.. (n + k) c= (A |^.. n) ^^ (A |^ (k,l))
proof
let x be
object ;
TARSKI:def 3 ( not x in A |^.. (n + k) or x in (A |^.. n) ^^ (A |^ (k,l)) )
assume
x in A |^.. (n + k)
;
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;
verum
end;
(A |^.. n) ^^ (A |^ (k,l)) c= A |^.. (n + k)
hence
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
by A2, XBOOLE_0:def 10; verum