let n be non empty Nat; :: thesis:
let p be RelStr-yielding ManySortedSet of n + 1; :: thesis:
let ns be Subset of (n + 1); :: thesis:
let ne be Element of n + 1; :: thesis:
assume that
A1: ns = n and
A2: ne = n ; :: thesis:
set S = [:(product (p | ns)),(p . ne):];
set T = product p;
set CP = [: the carrier of (product (p | ns)), the carrier of (p . ne):];
set CPP = the carrier of (product p);
A3: dom (Carrier (p | ns)) = n by A1, PARTFUN1:def 2;

per cases ;

suppose A4: the carrier of (product p) is empty ; :: thesis:

then A5: product p is empty ;
not p is non-Empty by A4;
then consider r1 being 1-sorted such that
A6: r1 in rng p and
A7: r1 is empty by WAYBEL_3:def 7;
consider x being set such that
A8: x in dom p and
A9: r1 = p . x by A6, FUNCT_1:def 3;
x in n + 1 by A8, PARTFUN1:def 2;
then A10: x in n \/ {n} by AFINSQ_1:2;
A11: [:(product (p | ns)),(p . ne):] is empty

proof

per cases by A10, XBOOLE_0:def 3;

suppose A12: x in n ; :: thesis:

then A13: (p | ns) . x = p . x by A1, FUNCT_1:49;
x in dom (p | ns) by A1, A12, PARTFUN1:def 2;
then p . x in rng (p | ns) by A13, FUNCT_1:def 3;
then not p | ns is non-Empty by A7, A9, WAYBEL_3:def 7;
then reconsider ptemp = the carrier of (product (p | ns)) as empty set by A1, Th41;
[:ptemp, the carrier of (p . ne):] is empty ;
hence [:(product (p | ns)),(p . ne):] is empty by YELLOW_3:def 2; :: thesis:

end;

suppose x in {n} ; :: thesis:

then p . ne is empty by A2, A7, A9, TARSKI:def 1;
then reconsider pne = the carrier of (p . ne) as empty set ;
reconsider ptemp = the carrier of (product (p | ns)) as set ;
[:ptemp,pne:] is empty ;
hence [:(product (p | ns)),(p . ne):] is empty by YELLOW_3:def 2; :: thesis:

end;

then A14: dom {} = the carrier of [:(product (p | ns)),(p . ne):] ;
for x being set st x in {} holds
{} . x in the carrier of (product p) ;
then reconsider f = {} as Function of [:(product (p | ns)),(p . ne):],(product p) by A14, FUNCT_2:3;
f is isomorphic by A5, A11, WAYBEL_0:def 38;
hence [:(product (p | ns)),(p . ne):], product p are_isomorphic by WAYBEL_1:def 8; :: thesis:

end;

suppose A15: not the carrier of (product p) is empty ; :: thesis:

then reconsider CPP = the carrier of (product p) as non empty set ;
reconsider T = product p as non empty RelStr by A15;
A16: p is non-Empty by A15, Th41;
reconsider p9 = p as RelStr-yielding non-Empty ManySortedSet of n + 1 by A15, Th41;
not p9 . ne is empty ;
then reconsider pne2 = the carrier of (p . ne) as non empty set ;

now

let S be 1-sorted ; :: thesis:
assume S in rng (p | ns) ; :: thesis:
then consider x being set such that
A17: x in dom (p | ns) and
A18: S = (p | ns) . x by FUNCT_1:def 3;
x in ns by A17, PARTFUN1:def 2;
then x in n + 1 ;
then A19: x in dom p by PARTFUN1:def 2;
S = p . x by A17, A18, FUNCT_1:47;
then S in rng p by A19, FUNCT_1:def 3;
hence not S is empty by A16, WAYBEL_3:def 7; :: thesis:

end;

then A20: p | ns is non-Empty by WAYBEL_3:def 7;
then A21: not product (p | ns) is empty ;
reconsider ppns2 = the carrier of (product (p | ns)) as non empty set by A20;
[: the carrier of (product (p | ns)), the carrier of (p . ne):] = [:ppns2,pne2:] ;
then reconsider S = [:(product (p | ns)),(p . ne):] as non empty RelStr by YELLOW_3:def 2;
[: the carrier of (product (p | ns)), the carrier of (p . ne):] = the carrier of S by YELLOW_3:def 2;
then reconsider CP9 = [: the carrier of (product (p | ns)), the carrier of (p . ne):] as non empty set ;
defpred S₁[ set , set ] means ex a being Function ex b being Element of pne2 st
( a in ppns2 & $1 = [a,b] & $2 = a +* (n .--> b) );
A22: for x being Element of CP9 ex y being Element of CPP st S₁[x,y]

proof

let x be Element of CP9; :: thesis:
reconsider xx = x as Element of [:ppns2,pne2:] ;
set a = xx `1 ;
set b = xx `2 ;
reconsider a = xx `1 as Element of ppns2 by MCART_1:10;
reconsider b = xx `2 as Element of pne2 by MCART_1:10;
A23: not product (Carrier (p | ns)) is empty by A21, YELLOW_1:def 4;
A24: a is Element of product (Carrier (p | ns)) by YELLOW_1:def 4;
then A25: ex g being Function st
( a = g & dom g = dom (Carrier (p | ns)) & ( for i being set st i in dom (Carrier (p | ns)) holds
g . i in (Carrier (p | ns)) . i ) ) by A23, CARD_3:def 5;
reconsider a = a as Function by A24;
set y = a +* (n .--> b);

now

set g1 = a +* (n .--> b);
reconsider g1 = a +* (n .--> b) as Function ;
take g1 = g1; :: thesis:
thus a +* (n .--> b) = g1 ; :: thesis:
A26: dom a = ns by A25, PARTFUN1:def 2;
A27: dom (n .--> b) = {n} by FUNCOP_1:13;
thus dom g1 = (dom a) \/ (dom (n .--> b)) by FUNCT_4:def 1
.= n \/ {n} by A1, A26, FUNCOP_1:13
.= n + 1 by AFINSQ_1:2
.= dom (Carrier p) by PARTFUN1:def 2 ; :: thesis:
let x be set ; :: thesis:
assume x in dom (Carrier p) ; :: thesis:
then A28: x in n + 1 by PARTFUN1:def 2;
then A29: x in n \/ {n} by AFINSQ_1:2;

per cases by A29, XBOOLE_0:def 3;

suppose A30: x in n ; :: thesis:

then x <> n ;
then not x in dom (n .--> b) by A27, TARSKI:def 1;
then A31: g1 . x = a . x by FUNCT_4:11;
A32: x in dom (Carrier (p | ns)) by A1, A30, PARTFUN1:def 2;
A33: ex R being 1-sorted st
( R = (p | ns) . x & (Carrier (p | ns)) . x = the carrier of R ) by A1, A30, PRALG_1:def 13;
ex R2 being 1-sorted st
( R2 = p . x & (Carrier p) . x = the carrier of R2 ) by A28, PRALG_1:def 13;
then (Carrier (p | ns)) . x = (Carrier p) . x by A1, A30, A33, FUNCT_1:49;
hence g1 . x in (Carrier p) . x by A25, A31, A32; :: thesis:

end;

suppose A34: x in {n} ; :: thesis:

then A35: x = n by TARSKI:def 1;
x in dom (n .--> b) by A34, FUNCOP_1:13;
then A36: g1 . x = (n .--> b) . n by A35, FUNCT_4:13
.= b by FUNCOP_1:72 ;
ex R being 1-sorted st
( R = p . ne & (Carrier p) . ne = the carrier of R ) by PRALG_1:def 13;
hence g1 . x in (Carrier p) . x by A2, A35, A36; :: thesis:

end;

then a +* (n .--> b) in product (Carrier p) by CARD_3:def 5;
then reconsider y = a +* (n .--> b) as Element of CPP by YELLOW_1:def 4;
take y ; :: thesis:
take a ; :: thesis:
take b ; :: thesis:
thus a in ppns2 ; :: thesis:
thus x = [a,b] by MCART_1:21; :: thesis:
thus y = a +* (n .--> b) ; :: thesis:

end;

consider f being Function of CP9,CPP such that
A37: for x being Element of CP9 holds S₁[x,f . x] from FUNCT_2:sch 3(A22);

now

the carrier of [:(product (p | ns)),(p . ne):] = [: the carrier of (product (p | ns)), the carrier of (p . ne):] by YELLOW_3:def 2;
then reconsider f = f as Function of [:(product (p | ns)),(p . ne):],(product p) ;
reconsider f9 = f as Function of S,T ;
take f = f; :: thesis:

now

let x1, x2 be set ; :: thesis:
assume that
A38: x1 in dom f and
A39: x2 in dom f and
A40: f . x1 = f . x2 ; :: thesis:
x1 is Element of [: the carrier of (product (p | ns)), the carrier of (p . ne):] by A38, YELLOW_3:def 2;
then consider a1 being Function, b1 being Element of pne2 such that
A41: a1 in ppns2 and
A42: x1 = [a1,b1] and
A43: f . x1 = a1 +* (n .--> b1) by A37;
x2 is Element of [: the carrier of (product (p | ns)), the carrier of (p . ne):] by A39, YELLOW_3:def 2;
then consider a2 being Function, b2 being Element of pne2 such that
A44: a2 in ppns2 and
A45: x2 = [a2,b2] and
A46: f . x2 = a2 +* (n .--> b2) by A37;
a1 in product (Carrier (p | ns)) by A41, YELLOW_1:def 4;
then A47: ex g1 being Function st
( a1 = g1 & dom g1 = dom (Carrier (p | ns)) & ( for x being set st x in dom (Carrier (p | ns)) holds
g1 . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
a2 in product (Carrier (p | ns)) by A44, YELLOW_1:def 4;
then A48: ex g2 being Function st
( a2 = g2 & dom g2 = dom (Carrier (p | ns)) & ( for x being set st x in dom (Carrier (p | ns)) holds
g2 . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
A49: dom (n .--> b1) = {n} by FUNCOP_1:13;
then A50: dom (n .--> b1) = dom (n .--> b2) by FUNCOP_1:13;
A51: dom a1 = n by A1, A47, PARTFUN1:def 2;

A52: now

assume not n misses {n} ; :: thesis:
then n /\ {n} <> {} by XBOOLE_0:def 7;
then consider x being set such that
A53: x in n /\ {n} by XBOOLE_0:def 1;
A54: x in n by A53, XBOOLE_0:def 4;
x in {n} by A53, XBOOLE_0:def 4;
then x = n by TARSKI:def 1;
hence contradiction by A54; :: thesis:

end;

then A55: dom a1 misses dom (n .--> b1) by A51, FUNCOP_1:13;
A56: dom a2 misses dom (n .--> b2) by A47, A48, A51, A52, FUNCOP_1:13;

A57: now

let a, b be set ; :: thesis:

hereby :: thesis:

assume A58: [a,b] in a1 ; :: thesis:
then A59: a in dom a1 by FUNCT_1:1;
A60: b = a1 . a by A58, FUNCT_1:1;
A61: a in (dom a1) \/ (dom (n .--> b1)) by A59, XBOOLE_0:def 3;
then not a in dom (n .--> b1) by A55, A59, XBOOLE_0:5;
then A62: (a2 +* (n .--> b2)) . a = a1 . a by A40, A43, A46, A61, FUNCT_4:def 1;
A63: a in (dom a2) \/ (dom (n .--> b2)) by A47, A48, A59, XBOOLE_0:def 3;
A64: a in dom a2 by A47, A48, A58, FUNCT_1:1;
then not a in dom (n .--> b2) by A56, A63, XBOOLE_0:5;
then b = a2 . a by A60, A62, A63, FUNCT_4:def 1;
hence [a,b] in a2 by A64, FUNCT_1:1; :: thesis:

end;

assume A65: [a,b] in a2 ; :: thesis:
then A66: a in dom a2 by FUNCT_1:1;
A67: b = a2 . a by A65, FUNCT_1:1;
A68: a in (dom a2) \/ (dom (n .--> b2)) by A66, XBOOLE_0:def 3;
then not a in dom (n .--> b2) by A56, A66, XBOOLE_0:5;
then A69: (a1 +* (n .--> b1)) . a = a2 . a by A40, A43, A46, A68, FUNCT_4:def 1;
A70: a in (dom a1) \/ (dom (n .--> b1)) by A47, A48, A66, XBOOLE_0:def 3;
A71: a in dom a1 by A47, A48, A65, FUNCT_1:1;
then not a in dom (n .--> b1) by A55, A70, XBOOLE_0:5;
then b = a1 . a by A67, A69, A70, FUNCT_4:def 1;
hence [a,b] in a1 by A71, FUNCT_1:1; :: thesis:

end;

A72: n in dom (n .--> b1) by A49, TARSKI:def 1;
then A73: n in (dom a1) \/ (dom (n .--> b1)) by XBOOLE_0:def 3;
A74: n in dom (n .--> b2) by A49, A50, TARSKI:def 1;
then n in (dom a2) \/ (dom (n .--> b2)) by XBOOLE_0:def 3;
then (a1 +* (n .--> b1)) . n = (n .--> b2) . n by A40, A43, A46, A74, FUNCT_4:def 1
.= b2 by FUNCOP_1:72 ;
then b2 = (n .--> b1) . n by A72, A73, FUNCT_4:def 1
.= b1 by FUNCOP_1:72 ;
hence x1 = x2 by A42, A45, A57, RELAT_1:def 2; :: thesis:

end;

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

now

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
A76: y = g and
A77: dom g = dom (Carrier p) and
A78: for x being set st x in dom (Carrier p) holds
g . x in (Carrier p) . x by CARD_3:def 5;
A79: dom (Carrier p) = n + 1 by PARTFUN1:def 2;
A80: n + 1 = { i where i is Element of NAT : i < n + 1 } by AXIOMS:4;
A81: n in NAT by ORDINAL1:def 12;
n < n + 1 by NAT_1:13;
then A82: n in n + 1 by A80, A81;
set a = g | n;
set b = g . n;
set x = [(g | n),(g . n)];
A83: dom (Carrier (p | ns)) = ns by PARTFUN1:def 2;
A84: dom (g | n) = (dom g) /\ n by RELAT_1:61
.= (n + 1) /\ n by A77, PARTFUN1:def 2 ;
then A85: dom (g | n) = n by Th2, XBOOLE_1:28;
A86: dom (g | n) = dom (Carrier (p | ns)) by A1, A83, A84, XBOOLE_1:28;

now

let x be set ; :: thesis:
assume x in dom (Carrier (p | ns)) ; :: thesis:
then A87: x in n by A1, PARTFUN1:def 2;
A88: n c= n + 1 by Th2;
A89: (g | n) . x = g . x by A87, FUNCT_1:49;
A90: g . x in (Carrier p) . x by A78, A79, A87, A88;
A91: ex R1 being 1-sorted st
( R1 = p . x & (Carrier p) . x = the carrier of R1 ) by A87, A88, PRALG_1:def 13;
ex R2 being 1-sorted st
( R2 = (p | ns) . x & (Carrier (p | ns)) . x = the carrier of R2 ) by A1, A87, PRALG_1:def 13;
hence (g | n) . x in (Carrier (p | ns)) . x by A1, A87, A89, A90, A91, FUNCT_1:49; :: thesis:

end;

then g | n in product (Carrier (p | ns)) by A86, CARD_3:9;
then A92: g | n in the carrier of (product (p | ns)) by YELLOW_1:def 4;
ex R1 being 1-sorted st
( R1 = p . n & (Carrier p) . n = the carrier of R1 ) by A82, PRALG_1:def 13;
then A93: g . n in the carrier of (p . ne) by A2, A78, A79;
then [(g | n),(g . n)] in [: the carrier of (product (p | ns)), the carrier of (p . ne):] by A92, ZFMISC_1:87;
then A94: [(g | n),(g . n)] in dom f by FUNCT_2:def 1;
[(g | n),(g . n)] is Element of CP9 by A92, A93, ZFMISC_1:87;
then consider ta being Function, tb being Element of pne2 such that
ta in ppns2 and
A95: [(g | n),(g . n)] = [ta,tb] and
A96: f . [(g | n),(g . n)] = ta +* (n .--> tb) by A37;
A97: ta = g | n by A95, ZFMISC_1:27;
A98: tb = g . n by A95, ZFMISC_1:27;

now

let i, j be set ; :: thesis:

hereby :: thesis:

assume A99: [i,j] in (g | n) +* (n .--> (g . n)) ; :: thesis:
then i in dom ((g | n) +* (n .--> (g . n))) by FUNCT_1:1;
then A100: i in (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1;
then A101: i in n \/ {n} by A85, FUNCOP_1:13;
A102: ((g | n) +* (n .--> (g . n))) . i = j by A99, FUNCT_1:1;

per cases ;

suppose A103: i in dom (n .--> (g . n)) ; :: thesis:

then i in {n} by FUNCOP_1:13;
then A104: i = n by TARSKI:def 1;
((g | n) +* (n .--> (g . n))) . i = (n .--> (g . n)) . i by A100, A103, FUNCT_4:def 1
.= g . n by A104, FUNCOP_1:72 ;
then A105: g . i = j by A99, A104, FUNCT_1:1;
i in dom g by A77, A79, A101, AFINSQ_1:2;
hence [i,j] in g by A105, FUNCT_1:1; :: thesis:

end;

suppose A106: not i in dom (n .--> (g . n)) ; :: thesis:

then not i in {n} by FUNCOP_1:13;
then A107: i in n by A101, XBOOLE_0:def 3;
((g | n) +* (n .--> (g . n))) . i = (g | n) . i by A100, A106, FUNCT_4:def 1;
then A108: g . i = j by A102, A107, FUNCT_1:49;
i in dom g by A77, A79, A101, AFINSQ_1:2;
hence [i,j] in g by A108, FUNCT_1:1; :: thesis:

end;

assume A109: [i,j] in g ; :: thesis:
then A110: i in n + 1 by A77, A79, FUNCT_1:1;
then A111: i in n \/ {n} by AFINSQ_1:2;
dom ((g | n) +* (n .--> (g . n))) = (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1
.= n \/ {n} by A85, FUNCOP_1:13 ;
then A112: i in dom ((g | n) +* (n .--> (g . n))) by A110, AFINSQ_1:2;
then A113: i in (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1;

per cases ;

suppose A114: i in dom (n .--> (g . n)) ; :: thesis:

then i in {n} by FUNCOP_1:13;
then A115: i = n by TARSKI:def 1;
((g | n) +* (n .--> (g . n))) . i = (n .--> (g . n)) . i by A113, A114, FUNCT_4:def 1
.= g . n by A115, FUNCOP_1:72
.= j by A109, A115, FUNCT_1:1 ;
hence [i,j] in (g | n) +* (n .--> (g . n)) by A112, FUNCT_1:1; :: thesis:

end;

suppose A116: not i in dom (n .--> (g . n)) ; :: thesis:

then not i in {n} by FUNCOP_1:13;
then A117: i in n by A111, XBOOLE_0:def 3;
((g | n) +* (n .--> (g . n))) . i = (g | n) . i by A113, A116, FUNCT_4:def 1
.= g . i by A117, FUNCT_1:49
.= j by A109, FUNCT_1:1 ;
hence [i,j] in (g | n) +* (n .--> (g . n)) by A112, FUNCT_1:1; :: thesis:

end;

then f . [(g | n),(g . n)] = y by A76, A96, A97, A98, RELAT_1:def 2;
hence y in rng f by A94, FUNCT_1:def 3; :: thesis:

end;

then A118: rng f = the carrier of (product p) by TARSKI:1;

now

hereby :: thesis:

assume x <= y ; :: thesis:
then [x,y] in the InternalRel of S by ORDERS_2:def 5;
then A138: [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by YELLOW_3:def 2;
then A139: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by YELLOW_3:10;
A140: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A138, YELLOW_3:10;
A141: [xa,ya] in the InternalRel of (product (p | ns)) by A125, A127, A128, A129, A139, MCART_1:def 1;
A142: xa in product (Carrier (p | ns)) by A120, YELLOW_1:def 4;
xa9 <= ya9 by A141, ORDERS_2:def 5;
then consider ffx, ggx being Function such that
A143: ffx = xa and
A144: ggx = ya and
A145: for i being set st i in n holds
ex RR being RelStr ex xxi, yyi being Element of RR st
( RR = (p | ns) . i & xxi = ffx . i & yyi = ggx . i & xxi <= yyi ) by A1, A142, YELLOW_1:def 4;
A146: [xb,yb] in the InternalRel of (p . ne) by A125, A127, A128, A130, A140, MCART_1:def 2;
reconsider xb9 = xb as Element of (p . ne) ;
reconsider yb9 = yb as Element of (p . ne) ;
A147: xb9 <= yb9 by A146, ORDERS_2:def 5;
ex f1, g1 being Function st
( f1 = f . x & g1 = f . y & ( for i being set st i in n + 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 ) ) )

proof

set f1 = xa +* (n .--> xb);
set g1 = ya +* (n .--> yb);
take xa +* (n .--> xb) ; :: thesis:
take ya +* (n .--> yb) ; :: thesis:
thus xa +* (n .--> xb) = f . x by A122; :: thesis:
thus ya +* (n .--> yb) = f . y by A126; :: thesis:
let i be set ; :: thesis:
assume A148: i in n + 1 ; :: thesis:
A149: i in n \/ {n} by A148, AFINSQ_1:2;
set R = p . i;
set xi = (xa +* (n .--> xb)) . i;
set yi = (ya +* (n .--> yb)) . i;
i in dom p by A148, PARTFUN1:def 2;
then p . i in rng p by FUNCT_1:def 3;
then reconsider R = p . i as RelStr by YELLOW_1:def 3;
A150: i in (dom xa) \/ (dom (n .--> xb)) by A134, A148, AFINSQ_1:2;

now

per cases ;

suppose A151: i in dom (n .--> xb) ; :: thesis:

then i in {n} by FUNCOP_1:13;
then A152: i = n by TARSKI:def 1;
(xa +* (n .--> xb)) . i = (n .--> xb) . i by A150, A151, FUNCT_4:def 1;
hence (xa +* (n .--> xb)) . i is Element of R by A2, A152, FUNCOP_1:72; :: thesis:

end;

suppose A153: not i in dom (n .--> xb) ; :: thesis:

then A154: not i in {n} by FUNCOP_1:13;
then A155: i in n by A149, XBOOLE_0:def 3;
A156: i in dom (Carrier (p | ns)) by A3, A149, A154, XBOOLE_0:def 3;
(xa +* (n .--> xb)) . i = xa . i by A150, A153, FUNCT_4:def 1;
then A157: (xa +* (n .--> xb)) . i in (Carrier (p | ns)) . i by A132, A156;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A1, A155, PRALG_1:def 13;
hence (xa +* (n .--> xb)) . i is Element of R by A1, A155, A157, FUNCT_1:49; :: thesis:

end;

then reconsider xi = (xa +* (n .--> xb)) . i as Element of R ;
A158: i in (dom ya) \/ (dom (n .--> yb)) by A137, A148, AFINSQ_1:2;

now

per cases ;

suppose A159: i in dom (n .--> yb) ; :: thesis:

then i in {n} by FUNCOP_1:13;
then A160: i = n by TARSKI:def 1;
(ya +* (n .--> yb)) . i = (n .--> yb) . i by A158, A159, FUNCT_4:def 1;
hence (ya +* (n .--> yb)) . i is Element of R by A2, A160, FUNCOP_1:72; :: thesis:

end;

suppose A161: not i in dom (n .--> yb) ; :: thesis:

then A162: not i in {n} by FUNCOP_1:13;
then A163: i in n by A149, XBOOLE_0:def 3;
A164: i in dom (Carrier (p | ns)) by A3, A149, A162, XBOOLE_0:def 3;
(ya +* (n .--> yb)) . i = ya . i by A158, A161, FUNCT_4:def 1;
then A165: (ya +* (n .--> yb)) . i in (Carrier (p | ns)) . i by A135, A164;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A1, A163, PRALG_1:def 13;
hence (ya +* (n .--> yb)) . i is Element of R by A1, A163, A165, FUNCT_1:49; :: thesis:

end;

then reconsider yi = (ya +* (n .--> yb)) . i as Element of R ;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
thus R = p . i ; :: thesis:
thus xi = (xa +* (n .--> xb)) . i ; :: thesis:
thus yi = (ya +* (n .--> yb)) . i ; :: thesis:

per cases by A149, XBOOLE_0:def 3;

suppose A166: i in n ; :: thesis:

A167: not i in {n}

proof

assume i in {n} ; :: thesis:
then n in n by A166, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

then A168: not i in dom (n .--> xb) by FUNCOP_1:13;
not i in dom (n .--> yb) by A167, FUNCOP_1:13;
then A169: yi = ya . i by A158, FUNCT_4:def 1;
consider RR being RelStr , xxi, yyi being Element of RR such that
A170: RR = (p | ns) . i and
A171: xxi = ffx . i and
A172: yyi = ggx . i and
A173: xxi <= yyi by A145, A166;
RR = R by A1, A166, A170, FUNCT_1:49;
hence xi <= yi by A143, A144, A150, A168, A169, A171, A172, A173, FUNCT_4:def 1; :: thesis:

end;

suppose A174: i in {n} ; :: thesis:

then A175: i = n by TARSKI:def 1;
A176: i in dom (n .--> xb) by A174, FUNCOP_1:13;
A177: i in dom (n .--> yb) by A174, FUNCOP_1:13;
A178: xi = (n .--> xb) . i by A150, A176, FUNCT_4:def 1
.= xb by A175, FUNCOP_1:72 ;
yi = (n .--> yb) . i by A158, A177, FUNCT_4:def 1
.= yb by A175, FUNCOP_1:72 ;
hence xi <= yi by A2, A147, A174, A178, TARSKI:def 1; :: thesis:

end;

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

end;

assume f9 . x <= f9 . y ; :: thesis:
then consider f1, g1 being Function such that
A179: f1 = f . x and
A180: g1 = f . y and
A181: for i being set st i in n + 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 A123, YELLOW_1:def 4;

now

set f2 = xa9;
set g2 = ya9;
reconsider f2 = xa9, g2 = ya9 as Function ;
take f2 = f2; :: thesis:
take g2 = g2; :: thesis:
thus ( f2 = xa9 & g2 = ya9 ) ; :: thesis:
let i be set ; :: thesis:
assume A182: i in ns ; :: thesis:
A183: not i in {n}

proof

assume i in {n} ; :: thesis:
then i = n by TARSKI:def 1;
hence contradiction by A1, A182; :: thesis:

end;

then A184: not i in dom (n .--> yb) by FUNCOP_1:13;
A185: not i in dom (n .--> xb) by A183, FUNCOP_1:13;
set R = (p | ns) . i;
i in dom (p | ns) by A182, PARTFUN1:def 2;
then (p | ns) . i in rng (p | ns) by FUNCT_1:def 3;
then reconsider R = (p | ns) . i as RelStr by YELLOW_1:def 3;
take R = R; :: thesis:
set xi = xa . i;
set yi = ya . i;
A186: i in (dom xa) \/ (dom (n .--> xb)) by A1, A133, A182, XBOOLE_0:def 3;
A187: i in dom (Carrier (p | ns)) by A182, PARTFUN1:def 2;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A182, PRALG_1:def 13;
then reconsider xi = xa . i as Element of R by A132, A187;
A188: i in (dom ya) \/ (dom (n .--> yb)) by A1, A136, A182, XBOOLE_0:def 3;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A182, PRALG_1:def 13;
then reconsider yi = ya . i as Element of R by A135, A187;
take xi = xi; :: thesis:
take yi = yi; :: thesis:
thus ( R = (p | ns) . i & xi = f2 . i & yi = g2 . i ) ; :: thesis:
consider R2 being RelStr , xi2, yi2 being Element of R2 such that
A189: R2 = p . i and
A190: xi2 = f1 . i and
A191: yi2 = g1 . i and
A192: xi2 <= yi2 by A181, A182;
A193: R2 = R by A182, A189, FUNCT_1:49;
(xa +* (n .--> xb)) . i = xi by A185, A186, FUNCT_4:def 1;
hence xi <= yi by A122, A126, A179, A180, A184, A188, A190, A191, A192, A193, FUNCT_4:def 1; :: thesis:

end;

then xa9 <= ya9 by A131, YELLOW_1:def 4;
then [xa,ya] in the InternalRel of (product (p | ns)) by ORDERS_2:def 5;
then A194: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by A125, A127, A128, A129, MCART_1:def 1;
consider Rn being RelStr , xni, yni being Element of Rn such that
A195: Rn = p . ne and
A196: xni = f1 . n and
A197: yni = g1 . n and
A198: xni <= yni by A2, A181;
A199: [xni,yni] in the InternalRel of (p . ne) by A195, A198, ORDERS_2:def 5;
dom (n .--> xb) = {n} by FUNCOP_1:13;
then A200: n in dom (n .--> xb) by TARSKI:def 1;
then n in (dom xa) \/ (dom (n .--> xb)) by XBOOLE_0:def 3;
then A201: (xa +* (n .--> xb)) . n = (n .--> xb) . n by A200, FUNCT_4:def 1
.= xb by FUNCOP_1:72 ;
dom (n .--> yb) = {n} by FUNCOP_1:13;
then A202: n in dom (n .--> yb) by TARSKI:def 1;
then n in (dom ya) \/ (dom (n .--> yb)) by XBOOLE_0:def 3;
then (ya +* (n .--> yb)) . n = (n .--> yb) . n by A202, FUNCT_4:def 1
.= yb by FUNCOP_1:72 ;
then A203: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A122, A125, A126, A127, A128, A130, A179, A180, A196, A197, A199, A201, MCART_1:def 2;
A204: [x,y] `1 = [xa,xb] by A121, MCART_1:def 1;
[x,y] `2 = [ya,yb] by A125, MCART_1:def 2;
then [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by A194, A203, A204, YELLOW_3:10;
then [x,y] in the InternalRel of S by YELLOW_3:def 2;
hence x <= y by ORDERS_2:def 5; :: thesis:

end;

hence f is isomorphic by A75, A118, WAYBEL_0:66; :: thesis:

end;

hence [:(product (p | ns)),(p . ne):], product p are_isomorphic by WAYBEL_1:def 8; :: thesis:

end;