let n be non empty Nat; :: thesis: for p being RelStr-yielding ManySortedSet of holds
( not product p is empty iff p is non-Empty )
let p be RelStr-yielding ManySortedSet of ; :: thesis: ( not product p is empty iff p is non-Empty )

hereby :: thesis: ( p is non-Empty implies not product p is empty )

assume not product p is empty ; :: thesis: p is non-Empty
then not the carrier of (product p) is empty ;
then not product (Carrier p) is empty by YELLOW_1:def 4;
then consider z being set such that
A1: z in product (Carrier p) by XBOOLE_0:def 1;
consider g being Function such that
z = g and
dom g = dom (Carrier p) and
A2: for i being set st i in dom (Carrier p) holds
g . i in (Carrier p) . i by A1, CARD_3:def 5;

now

let S be 1-sorted ; :: thesis: ( S in rng p implies not S is empty )
assume A3: S in rng p ; :: thesis: not S is empty
consider x being set such that
A4: x in dom p and
A5: S = p . x by A3, FUNCT_1:def 5;
A6: x in n by A4, PARTFUN1:def 4;
then A7: x in dom (Carrier p) by PARTFUN1:def 4;
consider R being 1-sorted such that
A8: R = p . x and
A9: (Carrier p) . x = the carrier of R by A6, PRALG_1:def 13;
not the carrier of S is empty by A2, A5, A7, A8, A9;
hence not S is empty ; :: thesis: verum

end;

hence p is non-Empty by WAYBEL_3:def 7; :: thesis: verum

end;

assume A10: p is non-Empty ; :: thesis: not product p is empty
A11: dom (Carrier p) = n by PARTFUN1:def 4;
deffunc H₁( set ) -> Element of (Carrier p) . $1 = choose ((Carrier p) . $1);
consider g being Function such that
A12: dom g = dom (Carrier p) and
A13: for i being set st i in dom (Carrier p) holds
g . i = H₁(i) from FUNCT_1:sch 3();
set x = g;

now

take g = g; :: thesis: ( g = g & dom g = dom (Carrier p) & ( for i being set st i in dom (Carrier p) holds
g . i in (Carrier p) . i ) )
thus g = g ; :: thesis: ( dom g = dom (Carrier p) & ( for i being set st i in dom (Carrier p) holds
g . i in (Carrier p) . i ) )
thus dom g = dom (Carrier p) by A12; :: thesis: for i being set st i in dom (Carrier p) holds
g . i in (Carrier p) . i
thus for i being set st i in dom (Carrier p) holds
g . i in (Carrier p) . i :: thesis: verum

proof

let i be set ; :: thesis: ( i in dom (Carrier p) implies g . i in (Carrier p) . i )
assume A14: i in dom (Carrier p) ; :: thesis: g . i in (Carrier p) . i
i in dom p by A11, A14, PARTFUN1:def 4;
then A15: p . i in rng p by FUNCT_1:def 5;
then reconsider pi1 = p . i as RelStr by YELLOW_1:def 3;
not pi1 is empty by A10, A15, WAYBEL_3:def 7;
then A16: not the carrier of pi1 is empty ;
i in n by A14, PARTFUN1:def 4;
then consider R being 1-sorted such that
A17: ( R = p . i & (Carrier p) . i = the carrier of R ) by PRALG_1:def 13;
g . i = choose ((Carrier p) . i) by A13, A14;
hence g . i in (Carrier p) . i by A16, A17; :: thesis: verum

end;

end;

then not product (Carrier p) is empty by CARD_3:def 5;
then not the carrier of (product p) is empty by YELLOW_1:def 4;
hence not product p is empty ; :: thesis: verum