let E be set ; 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); for k being Nat st A c= B |^.. k holds
B |^.. k = (B \/ A) |^.. k
let k be Nat; ( 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
; B |^.. k = (B \/ A) |^.. k
A3:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A4:
S1[
n]
;
S1[n + 1]now ( n + 1 >= k implies (B \/ A) |^ (n + 1) c= B |^.. k )assume A5:
n + 1
>= k
;
(B \/ A) |^ (n + 1) c= B |^.. kper cases
( n + 1 = k or n >= k )
by A5, NAT_1:8;
suppose A9:
n >= k
;
(B \/ A) |^ (n + 1) c= B |^.. kA10:
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;
verum end; end; end; hence
S1[
n + 1]
;
verum end;
A14:
S1[ 0 ]
A17:
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A3);
A18:
(B \/ A) |^.. k c= B |^.. k
B |^.. k c= (B \/ A) |^.. k
by Th13, XBOOLE_1:7;
hence
B |^.. k = (B \/ A) |^.. k
by A18, XBOOLE_0:def 10; verum