let n be non zero Nat; :: thesis: for p being RelStr-yielding ManySortedSet of n holds
( not product p is empty iff p is non-Empty )
let p be RelStr-yielding ManySortedSet of n; :: 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 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;

now :: thesis: for S being 1-sorted st S in rng p holds
not S is empty

let S be 1-sorted ; :: thesis: ( S in rng p implies not S is empty )
assume S in rng p ; :: thesis: not S is empty
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: verum

end;

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

end;

assume A7: p is non-Empty ; :: thesis: not product p is empty
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;

now :: thesis: ex g being Function st
( g = g & dom g = dom (Carrier p) & ( for i being object st i in dom (Carrier p) holds
g . i in (Carrier p) . i ) )

take g = g; :: thesis: ( g = g & dom g = dom (Carrier p) & ( for i being object 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 object st i in dom (Carrier p) holds
g . i in (Carrier p) . i ) )
thus dom g = dom (Carrier p) by A9; :: thesis: for i being object st i in dom (Carrier p) holds
g . i in (Carrier p) . i
thus for i being object st i in dom (Carrier p) holds
g . i in (Carrier p) . i :: thesis: verum

proof

let i be object ; :: thesis: ( i in dom (Carrier p) implies g . i in (Carrier p) . i )
assume A11: i in dom (Carrier p) ; :: thesis: g . i in (Carrier p) . i
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: verum

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: verum