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;
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, Th40;
[: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, Th40;
reconsider p9 = p as RelStr-yielding non-Empty ManySortedSet of n + 1 by A15, Th40;
not p9 . ne is empty ;
then reconsider pne2 = the carrier of (p . ne) as non empty set ;

now :: thesis:

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;
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 :: thesis:

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;
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 A27: x in n + 1 ;
then A28: x in n \/ {n} by AFINSQ_1:2;

per cases by A28, XBOOLE_0:def 3;

suppose A29: x in n ; :: thesis:

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

end;

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

then A34: x = n by TARSKI:def 1;
x in dom (n .--> b) by A33, FUNCOP_1:13;
then A35: g1 . x = (n .--> b) . n by A34, 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, A34, A35; :: 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
A36: for x being Element of CP9 holds S₁[x,f . x] from FUNCT_2:sch 3(A22);

now :: thesis:

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

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

A51: now :: thesis:

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

end;

then A54: dom a1 misses dom (n .--> b1) by A50, FUNCOP_1:13;
A55: dom a2 misses dom (n .--> b2) by A46, A47, A50, A51, FUNCOP_1:13;

A56: now :: thesis:

let a, b be set ; :: thesis:

hereby :: thesis:

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

end;

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

end;

A71: n in dom (n .--> b1) by A48, TARSKI:def 1;
then A72: n in (dom a1) \/ (dom (n .--> b1)) by XBOOLE_0:def 3;
A73: n in dom (n .--> b2) by A48, A49, 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 A39, A42, A45, A73, FUNCT_4:def 1
.= b2 by FUNCOP_1:72 ;
then b2 = (n .--> b1) . n by A71, A72, FUNCT_4:def 1
.= b1 by FUNCOP_1:72 ;
hence x1 = x2 by A41, A44, A56, RELAT_1:def 2; :: thesis:

end;

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

now :: thesis:

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

now :: thesis:

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

end;

then g | n in product (Carrier (p | ns)) by A85, CARD_3:9;
then A91: 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 A81, PRALG_1:def 13;
then A92: g . n in the carrier of (p . ne) by A2, A77, A78;
then [(g | n),(g . n)] in [: the carrier of (product (p | ns)), the carrier of (p . ne):] by A91, ZFMISC_1:87;
then A93: [(g | n),(g . n)] in dom f by FUNCT_2:def 1;
[(g | n),(g . n)] is Element of CP9 by A91, A92, ZFMISC_1:87;
then consider ta being Function, tb being Element of pne2 such that
ta in ppns2 and
A94: [(g | n),(g . n)] = [ta,tb] and
A95: f . [(g | n),(g . n)] = ta +* (n .--> tb) by A36;
A96: ta = g | n by A94, XTUPLE_0:1;
A97: tb = g . n by A94, XTUPLE_0:1;

now :: thesis:

let i, j be set ; :: thesis:

hereby :: thesis:

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

per cases ;

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

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

end;

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

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

end;

assume A108: [i,j] in g ; :: thesis:
then A109: i in n + 1 by A76, A78, FUNCT_1:1;
then A110: 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 A84, FUNCOP_1:13 ;
then A111: i in dom ((g | n) +* (n .--> (g . n))) by A109, AFINSQ_1:2;
then A112: i in (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1;

per cases ;

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

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

end;

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

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

end;

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

end;

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

now :: thesis:

let x, y be Element of S; :: thesis:
A118: x is Element of [: the carrier of (product (p | ns)), the carrier of (p . ne):] by YELLOW_3:def 2;
then consider xa being Function, xb being Element of pne2 such that
A119: xa in ppns2 and
A120: x = [xa,xb] and
A121: f . x = xa +* (n .--> xb) by A36;
dom f = CP9 by FUNCT_2:def 1;
then f . x in the carrier of (product p) by A117, A118, FUNCT_1:def 3;
then A122: f9 . x in product (Carrier p) by YELLOW_1:def 4;
y is Element of [: the carrier of (product (p | ns)), the carrier of (p . ne):] by YELLOW_3:def 2;
then consider ya being Function, yb being Element of pne2 such that
A123: ya in ppns2 and
A124: y = [ya,yb] and
A125: f . y = ya +* (n .--> yb) by A36;
A126: [xa,xb] `1 = xa ;
A127: [xa,xb] `2 = xb ;
A128: xa in product (Carrier (p | ns)) by A119, YELLOW_1:def 4;
then A129: ex gx being Function st
( xa = gx & dom gx = dom (Carrier (p | ns)) & ( for x being set st x in dom (Carrier (p | ns)) holds
gx . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
then A130: dom xa = n by A1, PARTFUN1:def 2;
then A131: (dom xa) \/ (dom (n .--> xb)) = n \/ {n} by FUNCOP_1:13;
ya in product (Carrier (p | ns)) by A123, YELLOW_1:def 4;
then A132: ex gy being Function st
( ya = gy & dom gy = dom (Carrier (p | ns)) & ( for x being set st x in dom (Carrier (p | ns)) holds
gy . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
then A133: dom ya = n by A1, PARTFUN1:def 2;
then A134: (dom ya) \/ (dom (n .--> yb)) = n \/ {n} by FUNCOP_1:13;
reconsider xa9 = xa as Element of (product (p | ns)) by A119;
reconsider ya9 = ya as Element of (product (p | ns)) by A123;

hereby :: thesis:

assume x <= y ; :: thesis:
then [x,y] in the InternalRel of S by ORDERS_2:def 5;
then A135: [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by YELLOW_3:def 2;
then A136: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by YELLOW_3:10;
A137: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A135, YELLOW_3:10;
[ya,yb] `1 = ya ;
then A138: [xa,ya] in the InternalRel of (product (p | ns)) by A124, A126, A136, A120;
A139: xa in product (Carrier (p | ns)) by A119, YELLOW_1:def 4;
xa9 <= ya9 by A138, ORDERS_2:def 5;
then consider ffx, ggx being Function such that
A140: ffx = xa and
A141: ggx = ya and
A142: 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, A139, YELLOW_1:def 4;
[ya,yb] `2 = yb ;
then A143: [xb,yb] in the InternalRel of (p . ne) by A124, A127, A137, A120;
reconsider xb9 = xb as Element of (p . ne) ;
reconsider yb9 = yb as Element of (p . ne) ;
A144: xb9 <= yb9 by A143, 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 A121; :: thesis:
thus ya +* (n .--> yb) = f . y by A125; :: thesis:
let i be set ; :: thesis:
assume A145: i in n + 1 ; :: thesis:
A146: i in n \/ {n} by A145, AFINSQ_1:2;
set R = p . i;
set xi = (xa +* (n .--> xb)) . i;
set yi = (ya +* (n .--> yb)) . i;
i in dom p by A145, 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;
A147: i in (dom xa) \/ (dom (n .--> xb)) by A131, A145, AFINSQ_1:2;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

now :: thesis:

per cases ;

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

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

end;

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

then A159: not i in {n} by FUNCOP_1:13;
then A160: i in n by A146, XBOOLE_0:def 3;
A161: i in dom (Carrier (p | ns)) by A3, A146, A159, XBOOLE_0:def 3;
(ya +* (n .--> yb)) . i = ya . i by A155, A158, FUNCT_4:def 1;
then A162: (ya +* (n .--> yb)) . i in (Carrier (p | ns)) . i by A132, A161;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A1, A160, PRALG_1:def 13;
hence (ya +* (n .--> yb)) . i is Element of R by A1, A160, A162, 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 A146, XBOOLE_0:def 3;

suppose A163: i in n ; :: thesis:

A164: not i in {n}

proof

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

end;

then A165: not i in dom (n .--> xb) ;
not i in dom (n .--> yb) by A164;
then A166: yi = ya . i by A155, FUNCT_4:def 1;
consider RR being RelStr , xxi, yyi being Element of RR such that
A167: RR = (p | ns) . i and
A168: xxi = ffx . i and
A169: yyi = ggx . i and
A170: xxi <= yyi by A142, A163;
RR = R by A1, A163, A167, FUNCT_1:49;
hence xi <= yi by A140, A141, A147, A165, A166, A168, A169, A170, FUNCT_4:def 1; :: thesis:

end;

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

then A172: i = n by TARSKI:def 1;
A173: i in dom (n .--> xb) by A171, FUNCOP_1:13;
A174: i in dom (n .--> yb) by A171, FUNCOP_1:13;
A175: xi = (n .--> xb) . i by A147, A173, FUNCT_4:def 1
.= xb by A172, FUNCOP_1:72 ;
yi = (n .--> yb) . i by A155, A174, FUNCT_4:def 1
.= yb by A172, FUNCOP_1:72 ;
hence xi <= yi by A2, A144, A171, A175, TARSKI:def 1; :: thesis:

end;

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

end;

assume f9 . x <= f9 . y ; :: thesis:
then consider f1, g1 being Function such that
A176: f1 = f . x and
A177: g1 = f . y and
A178: 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 A122, YELLOW_1:def 4;

now :: thesis:

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 A179: i in ns ; :: thesis:
A180: not i in {n}

proof

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

end;

then A181: not i in dom (n .--> yb) ;
A182: not i in dom (n .--> xb) by A180;
set R = (p | ns) . i;
i in dom (p | ns) by A179, 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;
A183: i in (dom xa) \/ (dom (n .--> xb)) by A1, A130, A179, XBOOLE_0:def 3;
A184: i in dom (Carrier (p | ns)) by A179, PARTFUN1:def 2;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A179, PRALG_1:def 13;
then reconsider xi = xa . i as Element of R by A129, A184;
A185: i in (dom ya) \/ (dom (n .--> yb)) by A1, A133, A179, XBOOLE_0:def 3;
ex R2 being 1-sorted st
( R2 = (p | ns) . i & (Carrier (p | ns)) . i = the carrier of R2 ) by A179, PRALG_1:def 13;
then reconsider yi = ya . i as Element of R by A132, A184;
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
A186: R2 = p . i and
A187: xi2 = f1 . i and
A188: yi2 = g1 . i and
A189: xi2 <= yi2 by A178, A179;
A190: R2 = R by A179, A186, FUNCT_1:49;
(xa +* (n .--> xb)) . i = xi by A182, A183, FUNCT_4:def 1;
hence xi <= yi by A121, A125, A176, A177, A181, A185, A187, A188, A189, A190, FUNCT_4:def 1; :: thesis:

end;

then xa9 <= ya9 by A128, YELLOW_1:def 4;
then A191: [xa,ya] in the InternalRel of (product (p | ns)) by ORDERS_2:def 5;
[ya,yb] `1 = ya ;
then A192: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by A124, A126, A120, A191;
consider Rn being RelStr , xni, yni being Element of Rn such that
A193: Rn = p . ne and
A194: xni = f1 . n and
A195: yni = g1 . n and
A196: xni <= yni by A2, A178;
A197: [xni,yni] in the InternalRel of (p . ne) by A193, A196, ORDERS_2:def 5;
dom (n .--> xb) = {n} by FUNCOP_1:13;
then A198: n in dom (n .--> xb) by TARSKI:def 1;
then n in (dom xa) \/ (dom (n .--> xb)) by XBOOLE_0:def 3;
then A199: (xa +* (n .--> xb)) . n = (n .--> xb) . n by A198, FUNCT_4:def 1
.= xb by FUNCOP_1:72 ;
dom (n .--> yb) = {n} by FUNCOP_1:13;
then A200: n in dom (n .--> yb) by TARSKI:def 1;
then n in (dom ya) \/ (dom (n .--> yb)) by XBOOLE_0:def 3;
then A201: (ya +* (n .--> yb)) . n = (n .--> yb) . n by A200, FUNCT_4:def 1
.= yb by FUNCOP_1:72 ;
[ya,yb] `2 = yb ;
then A202: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A121, A124, A125, A127, A176, A177, A194, A195, A197, A199, A201, A120;
A203: [x,y] `1 = [xa,xb] by A120;
[x,y] `2 = [ya,yb] by A124;
then [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by A192, A202, A203, 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 A74, A117, WAYBEL_0:66; :: thesis:

end;

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

end;