let X, Z 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 A1: Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) } ; :: thesis:

now :: thesis:

let a be object ; :: thesis:
assume a in proj2 Z ; :: thesis:
then consider k being object such that
A2: [k,a] in Z by XTUPLE_0:def 13;
consider n being Nat, F being disjoint_valued FinSequence of P such that
A3: ( [k,a] = [n,F] & Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) by A1, A2;
thus a is FinSequence of P by A3, XTUPLE_0:1; :: thesis:

end;

hence proj2 Z is FinSequenceSet of P by FINSEQ_2:def 3; :: thesis:

hereby :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in rng K ; :: thesis:
then consider n being Element of NAT such that
A6: x = K . n by FUNCT_2:113;
K . n in Ring_generated_by P ;
then K . n in DisUnion P by SRINGS_3:18;
then consider A being Subset of X such that
A7: ( x = A & ex F being disjoint_valued FinSequence of P st A = Union F ) by A6;
consider F being disjoint_valued FinSequence of P such that
A8: A = Union F by A7;

per cases ;

suppose A9: K . n = {} ; :: thesis:

A10: rng <*{}*> = {{}} by FINSEQ_1:38;
{} in P by SETFAM_1:def 8;
then reconsider F1 = <*{}*> as disjoint_valued FinSequence of P by A10, ZFMISC_1:31, FINSEQ_1:def 4;
rng F1 = {{}} by FINSEQ_1:38;
then union (rng F1) = {} by ZFMISC_1:25;
then B1: Union F1 = {} by CARD_3:def 4;
then [n,F1] in Z by A9, A1;
then F1 in proj2 Z by XTUPLE_0:def 13;
hence ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) by A9, B1, A6; :: thesis:

end;

suppose K . n <> {} ; :: thesis:

then [n,F] in Z by A1, A6, A7, A8;
then F in proj2 Z by XTUPLE_0:def 13;
hence ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) by A8, A7; :: thesis:

end;

end;

end;

assume ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ; :: thesis:
then consider z being FinSequence of P such that
A12: ( z in proj2 Z & Union z = x ) ;
consider y being object such that
A13: [y,z] in Z by A12, XTUPLE_0:def 13;
consider n being Nat, F being disjoint_valued FinSequence of P such that
A14: ( [y,z] = [n,F] & Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) by A1, A13;
( y = n & z = F ) by A14, XTUPLE_0:1;
hence x in rng K by A12, A14, FUNCT_2:4, ORDINAL1:def 12; :: thesis:

end;

now :: thesis:

assume {} in proj2 Z ; :: thesis:
then consider y being object such that
A16: [y,{}] in Z by XTUPLE_0:def 13;
consider n being Nat, F being disjoint_valued FinSequence of P such that
A17: ( [y,{}] = [n,F] & Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) by A1, A16;
( y = n & {} = F ) by A17, XTUPLE_0:1;
then union (rng F) = {} by ZFMISC_1:2;
hence contradiction by A17, XTUPLE_0:1, CARD_3:def 4; :: thesis:

end;

hence proj2 Z is with_non-empty_elements ; :: thesis: