let E be set ; :: thesis: for A, B being Subset of (E ^omega)

for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

let A, B be Subset of (E ^omega); :: thesis: for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

let k be Nat; :: thesis: ( A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k )

defpred S_{1}[ Nat] means ( $1 >= k implies (B \/ A) |^ $1 c= B |^.. k );

B |^ 1 c= B |^.. 1 by Th3;

then A1: B c= B |^.. 1 by FLANG_1:25;

assume A2: A c= B |^.. k ; :: thesis: B |^.. k = (B \/ A) |^.. k

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A14, A3);

A18: (B \/ A) |^.. k c= B |^.. k

hence B |^.. k = (B \/ A) |^.. k by A18, XBOOLE_0:def 10; :: thesis: verum

for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

let A, B be Subset of (E ^omega); :: thesis: for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

let k be Nat; :: thesis: ( A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k )

defpred S

B |^ 1 c= B |^.. 1 by Th3;

then A1: B c= B |^.. 1 by FLANG_1:25;

assume A2: A c= B |^.. k ; :: thesis: B |^.. k = (B \/ A) |^.. k

A3: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A14:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A4: S

now :: thesis: ( n + 1 >= k implies (B \/ A) |^ (n + 1) c= B |^.. k )

hence
Sassume A5:
n + 1 >= k
; :: thesis: (B \/ A) |^ (n + 1) c= B |^.. k

end;per cases
( n + 1 = k or n >= k )
by A5, NAT_1:8;

end;

suppose A6:
n + 1 = k
; :: thesis: (B \/ A) |^ (n + 1) c= B |^.. k

end;

per cases
( k = 0 or k > 0 )
;

end;

suppose A7:
k > 0
; :: thesis: (B \/ A) |^ (n + 1) c= B |^.. k

then
k >= 0 + 1
by NAT_1:13;

then B |^.. k c= B |^.. 1 by Th5;

then A c= B |^.. 1 by A2;

then B \/ A c= B |^.. 1 by A1, XBOOLE_1:8;

then A8: (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:37;

(B |^.. 1) |^ k c= B |^.. (1 * k) by A7, Th19;

hence (B \/ A) |^ (n + 1) c= B |^.. k by A6, A8; :: thesis: verum

end;then B |^.. k c= B |^.. 1 by Th5;

then A c= B |^.. 1 by A2;

then B \/ A c= B |^.. 1 by A1, XBOOLE_1:8;

then A8: (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:37;

(B |^.. 1) |^ k c= B |^.. (1 * k) by A7, Th19;

hence (B \/ A) |^ (n + 1) c= B |^.. k by A6, A8; :: thesis: verum

suppose A9:
n >= k
; :: thesis: (B \/ A) |^ (n + 1) c= B |^.. k

A10:
B |^.. (k + k) c= B |^.. k
by Th5, NAT_1:11;

((B \/ A) |^ n) ^^ A c= B |^.. (k + k) by A2, A4, A9, Th21;

then A11: ((B \/ A) |^ n) ^^ A c= B |^.. k by A10;

A12: B |^.. (k + 1) c= B |^.. k by Th5, NAT_1:11;

((B \/ A) |^ n) ^^ B c= B |^.. (k + 1) by A1, A4, A9, Th21;

then A13: ((B \/ A) |^ n) ^^ B c= B |^.. k by A12;

(B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by FLANG_1:23

.= (((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A) by FLANG_1:20 ;

hence (B \/ A) |^ (n + 1) c= B |^.. k by A13, A11, XBOOLE_1:8; :: thesis: verum

end;((B \/ A) |^ n) ^^ A c= B |^.. (k + k) by A2, A4, A9, Th21;

then A11: ((B \/ A) |^ n) ^^ A c= B |^.. k by A10;

A12: B |^.. (k + 1) c= B |^.. k by Th5, NAT_1:11;

((B \/ A) |^ n) ^^ B c= B |^.. (k + 1) by A1, A4, A9, Th21;

then A13: ((B \/ A) |^ n) ^^ B c= B |^.. k by A12;

(B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by FLANG_1:23

.= (((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A) by FLANG_1:20 ;

hence (B \/ A) |^ (n + 1) c= B |^.. k by A13, A11, XBOOLE_1:8; :: thesis: verum

proof

A17:
for n being Nat holds S
assume
0 >= k
; :: thesis: (B \/ A) |^ 0 c= B |^.. k

then k = 0 ;

then A15: B |^.. k = B * by Th11;

A16: <%> E in B * by FLANG_1:48;

(B \/ A) |^ 0 = {(<%> E)} by FLANG_1:24;

hence (B \/ A) |^ 0 c= B |^.. k by A15, A16, ZFMISC_1:31; :: thesis: verum

end;then k = 0 ;

then A15: B |^.. k = B * by Th11;

A16: <%> E in B * by FLANG_1:48;

(B \/ A) |^ 0 = {(<%> E)} by FLANG_1:24;

hence (B \/ A) |^ 0 c= B |^.. k by A15, A16, ZFMISC_1:31; :: thesis: verum

A18: (B \/ A) |^.. k c= B |^.. k

proof

B |^.. k c= (B \/ A) |^.. k
by Th13, XBOOLE_1:7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B \/ A) |^.. k or x in B |^.. k )

assume x in (B \/ A) |^.. k ; :: thesis: x in B |^.. k

then consider n being Nat such that

A19: n >= k and

A20: x in (B \/ A) |^ n by Th2;

(B \/ A) |^ n c= B |^.. k by A17, A19;

hence x in B |^.. k by A20; :: thesis: verum

end;assume x in (B \/ A) |^.. k ; :: thesis: x in B |^.. k

then consider n being Nat such that

A19: n >= k and

A20: x in (B \/ A) |^ n by Th2;

(B \/ A) |^ n c= B |^.. k by A17, A19;

hence x in B |^.. k by A20; :: thesis: verum

hence B |^.. k = (B \/ A) |^.. k by A18, XBOOLE_0:def 10; :: thesis: verum