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 S1[ 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 S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[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 S1[n + 1] ; :: thesis: verum
end;
A14: S1[ 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 S1[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