let n be non zero Nat; :: thesis:
let p be RelStr-yielding ManySortedSet of Segm (n + 1); :: thesis:
let ns be Subset of (Segm (n + 1)); :: thesis:
let ne be Element of Segm (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 object such that
A8: x in dom p and
A9: r1 = p . x by A6, FUNCT_1:def 3;
x in Segm (n + 1) by A8;
then A10: x in (Segm 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, Th39;
[: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 object 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, Th39;
reconsider p9 = p as RelStr-yielding non-Empty ManySortedSet of Segm (n + 1) by A15, Th39;
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 object 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 object 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
.= (Segm n) \/ {n} by A1, A26
.= Segm (n + 1) by AFINSQ_1:2
.= dom (Carrier p) by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom (Carrier p) ; :: thesis:
then A27: x in Segm (n + 1) ;
then A28: x in (Segm n) \/ {n} by AFINSQ_1:2;

per cases by A28, XBOOLE_0:def 3;

suppose A29: x in n ; :: thesis:

x <> n

proof

assume A: x = n ; :: thesis:
then reconsider x = x as set ;
not x in x ;
hence contradiction by A, A29; :: thesis:

end;

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 15;
ex R2 being 1-sorted st
( R2 = p . x & (Carrier p) . x = the carrier of R2 ) by A27, PRALG_1:def 15;
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;
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 15;
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 object ; :: 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 object 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 object st x in dom (Carrier (p | ns)) holds
g2 . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
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 object 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 B: x = n by TARSKI:def 1;
then reconsider x = x as set ;
not x in n by B;
hence contradiction by A53; :: thesis:

end;

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

A56: now :: thesis:

let a, b be object ; :: 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 TARSKI:def 1;
then A72: n in (dom a1) \/ (dom (n .--> b1)) by XBOOLE_0:def 3;
A73: n in dom (n .--> b2) by 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 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
A75: y = g and
A76: dom g = dom (Carrier p) and
A77: for x being object 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 Nat : i < n + 1 } by AXIOMS:4;
n < n + 1 by NAT_1:13;
then A80: n in n + 1 by A79;
set a = g | n;
set b = g . n;
set x = [(g | n),(g . n)];
A81: dom (Carrier (p | ns)) = ns by PARTFUN1:def 2;
A82: dom (g | n) = (dom g) /\ (Segm n) by RELAT_1:61
.= (Segm (n + 1)) /\ (Segm n) by A76, PARTFUN1:def 2 ;
then A83: dom (g | n) = Segm n by NAT_1:63, XBOOLE_1:28;
A84: dom (g | n) = dom (Carrier (p | ns)) by A1, A81, A82, XBOOLE_1:28;

now :: thesis:

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

end;

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

now :: thesis:

let i, j be object ; :: thesis:

hereby :: thesis:

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

per cases ;

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

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

end;

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

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

end;

assume A107: [i,j] in g ; :: thesis:
then A108: i in Segm (n + 1) by A76, A78, FUNCT_1:1;
then A109: i in (Segm n) \/ {n} by AFINSQ_1:2;
dom ((g | n) +* (n .--> (g . n))) = (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1
.= (Segm n) \/ {n} by A83 ;
then A110: i in dom ((g | n) +* (n .--> (g . n))) by A108, AFINSQ_1:2;
then A111: i in (dom (g | n)) \/ (dom (n .--> (g . n))) by FUNCT_4:def 1;

per cases ;

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

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

end;

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

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

end;

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

end;

then A116: rng f = the carrier of (product p) by TARSKI:2;

now :: thesis:

let x, y be Element of S; :: thesis:
A117: 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
A118: xa in ppns2 and
A119: x = [xa,xb] and
A120: 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 A116, A117, FUNCT_1:def 3;
then A121: 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
A122: ya in ppns2 and
A123: y = [ya,yb] and
A124: f . y = ya +* (n .--> yb) by A36;
A125: xa in product (Carrier (p | ns)) by A118, YELLOW_1:def 4;
then A126: ex gx being Function st
( xa = gx & dom gx = dom (Carrier (p | ns)) & ( for x being object st x in dom (Carrier (p | ns)) holds
gx . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
then A127: dom xa = n by A1, PARTFUN1:def 2;
then A128: (dom xa) \/ (dom (n .--> xb)) = (Segm n) \/ {n} ;
ya in product (Carrier (p | ns)) by A122, YELLOW_1:def 4;
then A129: ex gy being Function st
( ya = gy & dom gy = dom (Carrier (p | ns)) & ( for x being object st x in dom (Carrier (p | ns)) holds
gy . x in (Carrier (p | ns)) . x ) ) by CARD_3:def 5;
then A130: dom ya = n by A1, PARTFUN1:def 2;
then A131: (dom ya) \/ (dom (n .--> yb)) = (Segm n) \/ {n} ;
reconsider xa9 = xa as Element of (product (p | ns)) by A118;
reconsider ya9 = ya as Element of (product (p | ns)) by A122;

hereby :: thesis:

assume x <= y ; :: thesis:
then [x,y] in the InternalRel of S ;
then A132: [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by YELLOW_3:def 2;
then A133: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by YELLOW_3:10;
A134: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A132, YELLOW_3:10;
A135: [xa,ya] in the InternalRel of (product (p | ns)) by A123, A133, A119;
A136: xa in product (Carrier (p | ns)) by A118, YELLOW_1:def 4;
xa9 <= ya9 by A135;
then consider ffx, ggx being Function such that
A137: ffx = xa and
A138: ggx = ya and
A139: for i being object 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, A136, YELLOW_1:def 4;
A140: [xb,yb] in the InternalRel of (p . ne) by A123, A134, A119;
reconsider xb9 = xb as Element of (p . ne) ;
reconsider yb9 = yb as Element of (p . ne) ;
A141: xb9 <= yb9 by A140;
ex f1, g1 being Function st
( f1 = f . x & g1 = f . y & ( for i being object st i in Segm (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 A120; :: thesis:
thus ya +* (n .--> yb) = f . y by A124; :: thesis:
let i be object ; :: thesis:
assume A142: i in Segm (n + 1) ; :: thesis:
A143: i in (Segm n) \/ {n} by A142, AFINSQ_1:2;
set R = p . i;
set xi = (xa +* (n .--> xb)) . i;
set yi = (ya +* (n .--> yb)) . i;
i in dom p by A142, 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;
A144: i in (dom xa) \/ (dom (n .--> xb)) by A128, A142, AFINSQ_1:2;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

now :: thesis:

per cases ;

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

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

end;

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

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

suppose A160: i in n ; :: thesis:

A161: not i in {n}

proof

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

end;

then A162: not i in dom (n .--> xb) ;
not i in dom (n .--> yb) by A161;
then A163: yi = ya . i by A152, FUNCT_4:def 1;
consider RR being RelStr , xxi, yyi being Element of RR such that
A164: RR = (p | ns) . i and
A165: xxi = ffx . i and
A166: yyi = ggx . i and
A167: xxi <= yyi by A139, A160;
RR = R by A1, A160, A164, FUNCT_1:49;
hence xi <= yi by A137, A138, A144, A162, A163, A165, A166, A167, FUNCT_4:def 1; :: thesis:

end;

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

then A169: i = n by TARSKI:def 1;
A170: i in dom (n .--> xb) by A168;
A171: i in dom (n .--> yb) by A168;
A172: xi = (n .--> xb) . i by A144, A170, FUNCT_4:def 1
.= xb by A169, FUNCOP_1:72 ;
yi = (n .--> yb) . i by A152, A171, FUNCT_4:def 1
.= yb by A169, FUNCOP_1:72 ;
hence xi <= yi by A2, A141, A168, A172, TARSKI:def 1; :: thesis:

end;

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

end;

assume f9 . x <= f9 . y ; :: thesis:
then consider f1, g1 being Function such that
A173: f1 = f . x and
A174: g1 = f . y and
A175: for i being object 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 A121, 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 object ; :: thesis:
assume A176: i in ns ; :: thesis:
A177: not i in {n}

proof

assume i in {n} ; :: thesis:
then A: i = n by TARSKI:def 1;
then reconsider i = i as set ;
not i in i ;
hence contradiction by A, A1, A176; :: thesis:

end;

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

end;

then xa9 <= ya9 by A125, YELLOW_1:def 4;
then A188: [xa,ya] in the InternalRel of (product (p | ns)) ;
A189: [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of (product (p | ns)) by A123, A119, A188;
consider Rn being RelStr , xni, yni being Element of Rn such that
A190: Rn = p . ne and
A191: xni = f1 . n and
A192: yni = g1 . n and
A193: xni <= yni by A2, A175;
A194: [xni,yni] in the InternalRel of (p . ne) by A190, A193;
A195: n in dom (n .--> xb) by TARSKI:def 1;
then n in (dom xa) \/ (dom (n .--> xb)) by XBOOLE_0:def 3;
then A196: (xa +* (n .--> xb)) . n = (n .--> xb) . n by A195, FUNCT_4:def 1
.= xb by FUNCOP_1:72 ;
A197: n in dom (n .--> yb) by TARSKI:def 1;
then n in (dom ya) \/ (dom (n .--> yb)) by XBOOLE_0:def 3;
then A198: (ya +* (n .--> yb)) . n = (n .--> yb) . n by A197, FUNCT_4:def 1
.= yb by FUNCOP_1:72 ;
A199: [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of (p . ne) by A120, A123, A124, A173, A174, A191, A192, A194, A196, A198, A119;
A200: [x,y] `1 = [xa,xb] by A119;
[x,y] `2 = [ya,yb] by A123;
then [x,y] in [" the InternalRel of (product (p | ns)), the InternalRel of (p . ne)"] by A189, A199, A200, YELLOW_3:10;
then [x,y] in the InternalRel of S by YELLOW_3:def 2;
hence x <= y ; :: thesis:

end;

hence f is isomorphic by A74, A116, WAYBEL_0:66; :: thesis:

end;

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

end;