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

let a be object ; :: thesis:
assume a in { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } ; :: thesis:
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:

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;

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

end;

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

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

end;

hence Y is with_non-empty_elements ; :: thesis: