let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being disjoint_valued FinSequence of S
for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for F being disjoint_valued FinSequence of S
for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R
let F be disjoint_valued FinSequence of S; :: thesis: for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R
let R be non empty preBoolean Subset-Family of X; :: thesis: ( S c= R & Union F in R implies for i being Nat holds Union (F | i) in R )
assume A1: ( S c= R & Union F in R ) ; :: thesis: for i being Nat holds Union (F | i) in R
defpred S1[ Nat] means Union (F | $1) in R;
union (rng (F | 0)) = {} by ZFMISC_1:2;
then Union (F | 0) = {} by CARD_3:def 4;
then A3: S1[ 0 ] by FINSUB_1:7;
A4: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; :: thesis: S1[i + 1]
per cases ( i >= len F or i < len F ) ;
suppose i >= len F ; :: thesis: S1[i + 1]
then ( F | i = F & F | (i + 1) = F ) by NAT_1:12, FINSEQ_1:58;
hence S1[i + 1] by A5; :: thesis: verum
end;
suppose i < len F ; :: thesis: S1[i + 1]
then A8: i + 1 <= len F by NAT_1:13;
set F1 = F | (i + 1);
A9: (F | (i + 1)) | i = F | i by NAT_1:12, FINSEQ_1:82;
F | (i + 1) = ((F | (i + 1)) | i) ^ <*((F | (i + 1)) . (i + 1))*> by A8, FINSEQ_1:17, FINSEQ_3:55;
then rng (F | (i + 1)) = (rng ((F | (i + 1)) | i)) \/ (rng <*((F | (i + 1)) . (i + 1))*>) by FINSEQ_1:31;
then rng (F | (i + 1)) = (rng (F | i)) \/ {((F | (i + 1)) . (i + 1))} by A9, FINSEQ_1:38;
then rng (F | (i + 1)) = (rng (F | i)) \/ {(F . (i + 1))} by FINSEQ_3:112;
then union (rng (F | (i + 1))) = (union (rng (F | i))) \/ (union {(F . (i + 1))}) by ZFMISC_1:78;
then Union (F | (i + 1)) = (union (rng (F | i))) \/ (union {(F . (i + 1))}) by CARD_3:def 4;
then Union (F | (i + 1)) = (Union (F | i)) \/ (union {(F . (i + 1))}) by CARD_3:def 4;
then A11: Union (F | (i + 1)) = (Union (F | i)) \/ (F . (i + 1)) by ZFMISC_1:25;
i + 1 in dom F by A8, NAT_1:12, FINSEQ_3:25;
then F . (i + 1) in rng F by FUNCT_1:3;
then F . (i + 1) in S ;
hence S1[i + 1] by A1, A5, A11, FINSUB_1:def 1; :: thesis: verum
end;
end;
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A3, A4);
 hence for i being Nat holds Union (F | i) in R ; :: thesis: verum