let n be non zero Nat; :: thesis:
let p be RelStr-yielding ManySortedSet of n; :: thesis:

hereby :: thesis:

assume not product p is empty ; :: thesis:
then not product (Carrier p) is empty by YELLOW_1:def 4;
then consider z being object such that
A1: z in product (Carrier p) by XBOOLE_0:def 1;
A2: ex g being Function st
( z = g & dom g = dom (Carrier p) & ( for i being object st i in dom (Carrier p) holds
g . i in (Carrier p) . i ) ) by A1, CARD_3:def 5;

let S be 1-sorted ; :: thesis:
assume S in rng p ; :: thesis:
then consider x being object such that
A3: x in dom p and
A4: S = p . x by FUNCT_1:def 3;
A5: x in n by A3;
then A6: x in dom (Carrier p) by PARTFUN1:def 2;
ex R being 1-sorted st
( R = p . x & (Carrier p) . x = the carrier of R ) by A5, PRALG_1:def 15;
hence not S is empty by A2, A4, A6; :: thesis:

end;

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

end;

assume A7: p is non-Empty ; :: thesis:
A8: dom (Carrier p) = n by PARTFUN1:def 2;
deffunc H₁( object ) -> Element of (Carrier p) . $1 = the Element of (Carrier p) . $1;
consider g being Function such that
A9: dom g = dom (Carrier p) and
A10: for i being object st i in dom (Carrier p) holds
g . i = H₁(i) from FUNCT_1:sch 3();
set x = g;

take g = g; :: thesis:
thus g = g ; :: thesis:
thus dom g = dom (Carrier p) by A9; :: thesis:
thus for i being object st i in dom (Carrier p) holds
g . i in (Carrier p) . i :: thesis:

let i be object ; :: thesis:
assume A11: i in dom (Carrier p) ; :: thesis:
i in dom p by A8, A11, PARTFUN1:def 2;
then A12: p . i in rng p by FUNCT_1:def 3;
then reconsider pi1 = p . i as RelStr by YELLOW_1:def 3;
not pi1 is empty by A7, A12, WAYBEL_3:def 7;
then A13: not the carrier of pi1 is empty ;
i in n by A11;
then A14: ex R being 1-sorted st
( R = p . i & (Carrier p) . i = the carrier of R ) by PRALG_1:def 15;
g . i = the Element of (Carrier p) . i by A10, A11;
hence g . i in (Carrier p) . i by A13, A14; :: thesis:

end;

end;

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