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 )
assume A1: A c= B |^.. k ; :: thesis: B |^.. k = (B \/ A) |^.. k
B |^ 1 c= B |^.. 1 by Th3;
then A2: B c= B |^.. 1 by FLANG_1:26;
defpred S₁[ Nat] means ( $1 >= k implies (B \/ A) |^ $1 c= B |^.. k );
A3: S₁[ 0 ]

proof

assume 0 >= k ; :: thesis: (B \/ A) |^ 0 c= B |^.. k
then k = 0 ;
then A4: B |^.. k = B * by Th11;
A5: (B \/ A) |^ 0 = {(<%> E)} by FLANG_1:25;
<%> E in B * by FLANG_1:49;
hence (B \/ A) |^ 0 c= B |^.. k by A4, A5, ZFMISC_1:37; :: thesis: verum

end;

A6: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]

now

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

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

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

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

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

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

end;

suppose A10: 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 A1, XBOOLE_1:1;
then B \/ A c= B |^.. 1 by A2, XBOOLE_1:8;
then A11: (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:38;
(B |^.. 1) |^ k c= B |^.. (1 * k) by A10, Th19;
hence (B \/ A) |^ (n + 1) c= B |^.. k by A9, A11, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

A13: (B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by FLANG_1:24
.= (((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A) by FLANG_1:21 ;
A14: ((B \/ A) |^ n) ^^ B c= B |^.. (k + 1) by A2, A7, A12, Th21;
B |^.. (k + 1) c= B |^.. k by Th5, NAT_1:11;
then A15: ((B \/ A) |^ n) ^^ B c= B |^.. k by A14, XBOOLE_1:1;
A16: ((B \/ A) |^ n) ^^ A c= B |^.. (k + k) by A1, A7, A12, Th21;
B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11;
then ((B \/ A) |^ n) ^^ A c= B |^.. k by A16, XBOOLE_1:1;
hence (B \/ A) |^ (n + 1) c= B |^.. k by A13, A15, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A17: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
A18: (B \/ A) |^.. k c= B |^.. k

proof

let x be set ; :: 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 & x in (B \/ A) |^ n ) by Th2;
(B \/ A) |^ n c= B |^.. k by A17, A19;
hence x in B |^.. k by A19; :: thesis: verum

end;

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