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

let x be set ; :: 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 } by FUNCOP_1:19
.= dom (Carrier p) by CARD_1:87, PARTFUN1:def 4 ;

let y be set ; :: thesis:
assume y in dom (Carrier p) ; :: thesis:
then A8: y in 1 by PARTFUN1:def 4;
then A9: y = 0 by CARD_1:87, TARSKI:def 1;
consider R being 1-sorted such that
A10: ( R = p . y & (Carrier p) . y = the carrier of R ) by A8, PRALG_1:def 13;
thus (0 .--> x) . y in (Carrier p) . y by A3, A5, A9, A10, FUNCOP_1:87; :: 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:5;

per cases ;

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

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

end;

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

end;

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

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

let i be set ; :: thesis:
assume A19: i in rng p ; :: thesis:
consider x being set such that
A20: x in dom p and
A21: i = p . x by A19, FUNCT_1:def 5;
x in 1 by A20, PARTFUN1:def 4;
then i = p . 0 by A21, CARD_1:87, TARSKI:def 1;
hence i is non empty 1-sorted by A18, CARD_1:87, TARSKI:def 1; :: thesis:

end;

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

let x1, x2 be set ; :: thesis:
assume that
A22: x1 in dom f and
A23: x2 in dom f and
A24: f . x1 = f . x2 ; :: thesis:
A25: f . x1 = 0 .--> x1 by A2, A22
.= [:{0 },{x1}:] ;
A26: f . x2 = 0 .--> x2 by A2, A23
.= [:{0 },{x2}:] ;
A27: 0 in {0 } by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then [0 ,x1] in f . x2 by A24, A25, A27, ZFMISC_1:def 2;
then consider xa, ya being set such that
xa in {0 } and
A28: ya in {x2} and
A29: [0 ,x1] = [xa,ya] by A26, ZFMISC_1:def 2;
x1 in {x2} by A28, A29, ZFMISC_1:33;
hence x1 = x2 by TARSKI:def 1; :: thesis:

end;

then A30: f is one-to-one by FUNCT_1:def 8;

let y be set ; :: 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
A31: y = g and
A32: dom g = dom (Carrier p) and
A33: for x being set st x in dom (Carrier p) holds
g . x in (Carrier p) . x by CARD_3:def 5;
A34: dom g = {0 } by A32, CARD_1:87, PARTFUN1:def 4;
A35: 0 in dom (Carrier p) by A4, PARTFUN1:def 4;
consider R being 1-sorted such that
A36: R = p . 0 and
A37: (Carrier p) . 0 = the carrier of R by A4, PRALG_1:def 13;
A38: g = 0 .--> (g . 0 ) by A34, Th1;
A39: f . (g . 0 ) = 0 .--> (g . 0 ) by A2, A3, A33, A35, A36, A37;
g . 0 in dom f by A1, A3, A33, A35, A36, A37;
hence y in rng f by A31, A38, A39, FUNCT_1:def 5; :: thesis:

end;

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

let x, y be Element of pz; :: thesis:
not product np is empty ;
then not the carrier of (product p) is empty ;
then A41: not product (Carrier p) is empty by YELLOW_1:def 4;
A42: f' . x is Element of product (Carrier p) by YELLOW_1:def 4;

hereby :: thesis:

assume A43: x <= y ; :: thesis:
ex f1, g1 being Function st
( f1 = f' . x & g1 = f' . y & ( for i being set st i in 1 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 = f' . x by A2; :: thesis:
thus g1 = f' . y by A2; :: thesis:
let i be set ; :: thesis:
assume A44: i in 1 ; :: thesis:
A45: i = 0 by A44, CARD_1:87, TARSKI:def 1;
0 in dom p by A4, PARTFUN1:def 4;
then p . 0 in rng p by FUNCT_1:def 5;
then reconsider p0 = p . 0 as RelStr by YELLOW_1:def 3;
set R = p0;
reconsider x' = x as Element of p0 by CARD_1:87, TARSKI:def 1;
reconsider y' = y as Element of p0 by CARD_1:87, TARSKI:def 1;
take p0 ; :: thesis:
take x' ; :: thesis:
take y' ; :: thesis:
thus p0 = p . i by A44, CARD_1:87, TARSKI:def 1; :: thesis:
thus x' = f1 . i by A45, FUNCOP_1:87; :: thesis:
thus y' = g1 . i by A45, FUNCOP_1:87; :: thesis:
thus x' <= y' by A43, CARD_1:87, TARSKI:def 1; :: thesis:

end;

hence f' . x <= f' . y by A41, A42, YELLOW_1:def 4; :: thesis:

end;

assume f' . x <= f' . y ; :: thesis:
then consider f1, g1 being Function such that
A46: f1 = f' . x and
A47: g1 = f' . y and
A48: for i being set st i in 1 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 A41, A42, YELLOW_1:def 4;
consider R being RelStr , xi, yi being Element of R such that
A49: R = p . 0 and
A50: xi = f1 . 0 and
A51: yi = g1 . 0 and
A52: xi <= yi by A4, A48;
f1 = 0 .--> x by A2, A46;
then A53: xi = x by A50, FUNCOP_1:87;
A54: g1 = 0 .--> y by A2, A47;
R = pz by A49, CARD_1:87, TARSKI:def 1;
hence x <= y by A51, A52, A53, A54, FUNCOP_1:87; :: thesis:

end;

hence f is isomorphic by A30, A40, WAYBEL_0:66; :: thesis:

end;

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