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 S₁[ 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: S₁[ 0 ] by FINSUB_1:7;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

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

per cases ( i >= len F or i < len F ) ;

suppose i >= len F ; :: thesis: S₁[i + 1]

then ( F | i = F & F | (i + 1) = F ) by NAT_1:12, FINSEQ_1:58;
hence S₁[i + 1] by A5; :: thesis: verum

end;

suppose i < len F ; :: thesis: S₁[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 S₁[i + 1] by A1, A5, A11, FINSUB_1:def 1; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
hence for i being Nat holds Union (F | i) in R ; :: thesis: verum