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₁[ 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

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

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

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

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

suppose A6: 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 A6; :: thesis: verum

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;

end;

end;

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;

end;

end;

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

end;

A14: S₁[ 0 ]

proof

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;

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

proof

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;

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