let p be RelStr-yielding ManySortedSet of {0}; :: thesis:
let z be Element of {0}; :: thesis:
deffunc H₁( object ) -> set = 0 .--> $1;
consider f being Function such that
A1: dom f = the carrier of (p . z) and
A2: for x being object st x in the carrier of (p . z) holds
f . x = H₁(x) from FUNCT_1:sch 3();
A3: z = 0 by TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;

let x be object ; :: thesis:
assume A5: x in the carrier of (p . z) ; :: thesis:
then A6: f . x = 0 .--> x by A2;
set g = 0 .--> x;
A7: dom (0 .--> x) = {0}
.= dom (Carrier p) by PARTFUN1:def 2 ;

let y be object ; :: thesis:
assume y in dom (Carrier p) ; :: thesis:
then A8: y in {0} ;
then A9: y = 0 by TARSKI:def 1;
ex R being 1-sorted st
( R = p . y & (Carrier p) . y = the carrier of R ) by A8, PRALG_1:def 15;
hence (0 .--> x) . y in (Carrier p) . y by A3, A5, A9; :: thesis:

end;

then f . x in product (Carrier p) by A6, A7, CARD_3:def 5;
hence f . x in the carrier of (product p) by YELLOW_1:def 4; :: thesis:

end;

then reconsider f = f as Function of (p . z),(product p) by A1, FUNCT_2:3;

suppose A10: p . z is empty ; :: thesis:

assume not the carrier of (product p) is empty ; :: thesis:
then A11: not product (Carrier p) is empty by YELLOW_1:def 4;
set x = the Element of product (Carrier p);
A12: ex g being Function st
( the Element of product (Carrier p) = g & dom g = dom (Carrier p) & ( for y being object st y in dom (Carrier p) holds
g . y in (Carrier p) . y ) ) by A11, CARD_3:def 5;
A13: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;
consider R being 1-sorted such that
A14: R = p . 0 and
A15: (Carrier p) . 0 = the carrier of R by A4, PRALG_1:def 15;
R is empty by A10, A14, TARSKI:def 1;
hence contradiction by A12, A13, A15; :: thesis:

end;

then product p is empty ;
hence f is isomorphic by A10, WAYBEL_0:def 38; :: thesis:

end;

suppose A16: not p . z is empty ; :: thesis:

then reconsider pz = p . z as non empty RelStr ;

let i be set ; :: thesis:
assume i in rng p ; :: thesis:
then consider x being object such that
A17: x in dom p and
A18: i = p . x by FUNCT_1:def 3;
x in {0} by A17;
then i = p . 0 by A18, TARSKI:def 1;
hence i is non empty 1-sorted by A16, TARSKI:def 1; :: thesis:

end;

then reconsider np = p as RelStr-yielding yielding_non-empty_carriers ManySortedSet of {0} by YELLOW_6:def 2;
not product np is empty ;
then reconsider pp = product p as non empty RelStr ;

let x1, x2 be object ; :: thesis:
assume that
A19: x1 in dom f and
A20: x2 in dom f and
A21: f . x1 = f . x2 ; :: thesis:
A22: f . x1 = 0 .--> x1 by A2, A19
.= [:{0},{x1}:] ;
A23: f . x2 = 0 .--> x2 by A2, A20
.= [:{0},{x2}:] ;
A24: 0 in {0} by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then [0,x1] in f . x2 by A21, A22, A24, ZFMISC_1:def 2;
then ex xa, ya being object st
( xa in {0} & ya in {x2} & [0,x1] = [xa,ya] ) by A23, ZFMISC_1:def 2;
then x1 in {x2} by XTUPLE_0:1;
hence x1 = x2 by TARSKI:def 1; :: thesis:

end;

then A25: f is one-to-one by FUNCT_1:def 4;

let y be object ; :: thesis:
thus ( y in rng f implies y in the carrier of (product p) ) ; :: thesis:
assume y in the carrier of (product p) ; :: thesis:
then y in product (Carrier p) by YELLOW_1:def 4;
then consider g being Function such that
A26: y = g and
A27: dom g = dom (Carrier p) and
A28: for x being object st x in dom (Carrier p) holds
g . x in (Carrier p) . x by CARD_3:def 5;
A29: dom g = {0} by A27, PARTFUN1:def 2;
A30: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;
A31: ex R being 1-sorted st
( R = p . 0 & (Carrier p) . 0 = the carrier of R ) by A4, PRALG_1:def 15;
A32: g = 0 .--> (g . 0) by A29, Th1;
A33: f . (g . 0) = 0 .--> (g . 0) by A2, A3, A28, A30, A31;
g . 0 in dom f by A1, A3, A28, A30, A31;
hence y in rng f by A26, A32, A33, FUNCT_1:def 3; :: thesis:

end;

then A34: rng f = the carrier of (product p) by TARSKI:2;
reconsider f9 = f as Function of pz,pp ;

let x, y be Element of pz; :: thesis:
not product np is empty ;
then A35: not product (Carrier p) is empty by YELLOW_1:def 4;
A36: f9 . x is Element of product (Carrier p) by YELLOW_1:def 4;

hereby :: thesis:

assume A37: x <= y ; :: thesis:
ex f1, g1 being Function st
( f1 = f9 . x & g1 = f9 . y & ( for i being object st i in {0} holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )

set f1 = 0 .--> x;
set g1 = 0 .--> y;
reconsider f1 = 0 .--> x as Function ;
reconsider g1 = 0 .--> y as Function ;
take f1 ; :: thesis:
take g1 ; :: thesis:
thus f1 = f9 . x by A2; :: thesis:
thus g1 = f9 . y by A2; :: thesis:
let i be object ; :: thesis:
assume A38: i in {0} ; :: thesis:
A39: i = 0 by A38, TARSKI:def 1;
0 in dom p by A4, PARTFUN1:def 2;
then p . 0 in rng p by FUNCT_1:def 3;
then reconsider p0 = p . 0 as RelStr by YELLOW_1:def 3;
set R = p0;
reconsider x9 = x as Element of p0 by TARSKI:def 1;
reconsider y9 = y as Element of p0 by TARSKI:def 1;
take p0 ; :: thesis:
take x9 ; :: thesis:
take y9 ; :: thesis:
thus p0 = p . i by A38, TARSKI:def 1; :: thesis:
thus x9 = f1 . i by A39, FUNCOP_1:72; :: thesis:
thus y9 = g1 . i by A39, FUNCOP_1:72; :: thesis:
thus x9 <= y9 by A37, TARSKI:def 1; :: thesis:

end;

hence f9 . x <= f9 . y by A35, A36, YELLOW_1:def 4; :: thesis:

end;

assume f9 . x <= f9 . y ; :: thesis:
then consider f1, g1 being Function such that
A40: f1 = f9 . x and
A41: g1 = f9 . y and
A42: for i being object st i in {0} holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A35, A36, YELLOW_1:def 4;
consider R being RelStr , xi, yi being Element of R such that
A43: R = p . 0 and
A44: xi = f1 . 0 and
A45: yi = g1 . 0 and
A46: xi <= yi by A4, A42;
f1 = 0 .--> x by A2, A40;
then A47: xi = x by A44, FUNCOP_1:72;
A48: g1 = 0 .--> y by A2, A41;
R = pz by A43, TARSKI:def 1;
hence x <= y by A45, A46, A47, A48, FUNCOP_1:72; :: thesis:

end;

hence f is isomorphic by A25, A34, WAYBEL_0:66; :: thesis:

end;

end;

end;

hence p . z, product p are_isomorphic by WAYBEL_1:def 8; :: thesis: