let X be set ; :: thesis: for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT,(Ring_generated_by P) st rng K is with_non-empty_element holds
ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )
let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for K being disjoint_valued Function of NAT,(Ring_generated_by P) st rng K is with_non-empty_element holds
ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )
let K be disjoint_valued Function of NAT,(Ring_generated_by P); :: thesis: ( rng K is with_non-empty_element implies ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements ) )
assume A0: rng K is with_non-empty_element ; :: thesis: ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )
set Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } ;

now :: thesis: for a being object st a in { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } holds
a is FinSequence of P

let a be object ; :: thesis: ( a in { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } implies a is FinSequence of P )
assume a in { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } ; :: thesis: a is FinSequence of P
then ex A being disjoint_valued FinSequence of P st
( a = A & Union A in rng K & A <> {} ) ;
hence a is FinSequence of P ; :: thesis: verum

end;

then reconsider Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } as FinSequenceSet of P by FINSEQ_2:def 3;
consider k being non empty set such that
A2: k in rng K by A0;
consider i being Element of NAT such that
A3: k = K . i by A2, FUNCT_2:113;
K . i in Ring_generated_by P ;
then K . i in DisUnion P by SRINGS_3:18;
then consider A being Subset of X such that
A4: ( K . i = A & ex F being disjoint_valued FinSequence of P st A = Union F ) ;
consider F being disjoint_valued FinSequence of P such that
A5: A = Union F by A4;

now :: thesis: not F = {}

assume F = {} ; :: thesis: contradiction
then union (rng F) = {} by ZFMISC_1:2;
hence contradiction by A5, A4, A3, CARD_3:def 4; :: thesis: verum

end;

then F in Y by A2, A3, A4, A5;
then reconsider Y = Y as non empty FinSequenceSet of P ;
take Y ; :: thesis: ( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )
thus Y = { A where A is disjoint_valued FinSequence of P : ( Union A in rng K & A <> {} ) } ; :: thesis: Y is with_non-empty_elements

now :: thesis: not {} in Y

assume {} in Y ; :: thesis: contradiction
then ex A being disjoint_valued FinSequence of P st
( {} = A & Union A in rng K & A <> {} ) ;
hence contradiction ; :: thesis: verum

end;

hence Y is with_non-empty_elements ; :: thesis: verum