let n be non empty Nat; :: thesis: for p being RelStr-yielding ManySortedSet of
for ns being Subset of (n + 1)
for ne being Element of n + 1 st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic
let p be RelStr-yielding ManySortedSet of ; :: thesis: for ns being Subset of (n + 1)
for ne being Element of n + 1 st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic
let ns be Subset of (n + 1); :: thesis: for ne being Element of n + 1 st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic
let ne be Element of n + 1; :: thesis: ( ns = n & ne = n implies [:(product (p | ns)),(p . ne):], product p are_isomorphic )
assume that
A1:
ns = n
and
A2:
ne = n
; :: thesis: [:(product (p | ns)),(p . ne):], product p are_isomorphic
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 4;
per cases
( the carrier of (product p) is empty or not the carrier of (product p) is empty )
;
suppose
the
carrier of
(product p) is
empty
;
:: thesis: [:(product (p | ns)),(p . ne):], product p are_isomorphic then A4:
product p is
empty
;
then
not
p is
non-Empty
;
then consider r1 being
1-sorted such that A5:
r1 in rng p
and A6:
r1 is
empty
by WAYBEL_3:def 7;
consider x being
set such that A7:
x in dom p
and A8:
r1 = p . x
by A5, FUNCT_1:def 5;
x in n + 1
by A7, PARTFUN1:def 4;
then A9:
x in n \/ {n}
by AFINSQ_1:4;
A10:
[:(product (p | ns)),(p . ne):] is
empty
proof
per cases
( x in n or x in {n} )
by A9, XBOOLE_0:def 3;
suppose A11:
x in n
;
:: thesis: [:(product (p | ns)),(p . ne):] is empty then A12:
(p | ns) . x = p . x
by A1, FUNCT_1:72;
x in dom (p | ns)
by A1, A11, PARTFUN1:def 4;
then
p . x in rng (p | ns)
by A12, FUNCT_1:def 5;
then
not
p | ns is
non-Empty
by A6, A8, WAYBEL_3:def 7;
then
product (p | ns) is
empty
by A1, Th41;
then reconsider ptemp = the
carrier of
(product (p | ns)) as
empty set ;
[:ptemp,the carrier of (p . ne):] is
empty
;
then
the
carrier of
[:(product (p | ns)),(p . ne):] is
empty
by YELLOW_3:def 2;
hence
[:(product (p | ns)),(p . ne):] is
empty
;
:: thesis: verum end;
end; consider f being
empty Function;
A13:
dom f = the
carrier of
[:(product (p | ns)),(p . ne):]
by A10;
for
x being
set st
x in {} holds
f . x in the
carrier of
(product p)
;
then reconsider f =
f as
Function of the
carrier of
[:(product (p | ns)),(p . ne):],the
carrier of
(product p) by A13, FUNCT_2:5;
reconsider f =
f as
Function of
[:(product (p | ns)),(p . ne):],
(product p) ;
f is
isomorphic
by A4, A10, WAYBEL_0:def 38;
hence
[:(product (p | ns)),(p . ne):],
product p are_isomorphic
by WAYBEL_1:def 8;
:: thesis: verum end; suppose A14:
not the
carrier of
(product p) is
empty
;
:: thesis: [:(product (p | ns)),(p . ne):], product p are_isomorphic then reconsider CPP = the
carrier of
(product p) as non
empty set ;
reconsider T =
product p as non
empty RelStr by A14;
A15:
not
product p is
empty
by A14;
then A16:
p is
non-Empty
by Th41;
reconsider p' =
p as
RelStr-yielding non-Empty ManySortedSet of
by A15, Th41;
not
p' . ne is
empty
;
then reconsider pne2 = the
carrier of
(p . ne) as non
empty set ;
then
p | ns is
non-Empty
by WAYBEL_3:def 7;
then A21:
not
product (p | ns) is
empty
;
then A22:
not the
carrier of
(product (p | ns)) is
empty
;
reconsider ppns2 = the
carrier of
(product (p | ns)) as non
empty set by A21;
[:the carrier of (product (p | ns)),the carrier of (p . ne):] = [:ppns2,pne2:]
;
then
not the
carrier of
[:(product (p | ns)),(p . ne):] is
empty
by YELLOW_3:def 2;
then reconsider S =
[:(product (p | ns)),(p . ne):] as non
empty RelStr ;
[:the carrier of (product (p | ns)),the carrier of (p . ne):] = the
carrier of
S
by YELLOW_3:def 2;
then reconsider CP' =
[:the carrier of (product (p | ns)),the carrier of (p . ne):] as non
empty set ;
defpred S1[
set ,
set ]
means ex
a being
Function ex
b being
Element of
pne2 st
(
a in ppns2 & $1
= [a,b] & $2
= a +* (n .--> b) );
A23:
for
x being
Element of
CP' ex
y being
Element of
CPP st
S1[
x,
y]
proof
let x be
Element of
CP';
:: thesis: ex y being Element of CPP st S1[x,y]
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;
A24:
not
product (Carrier (p | ns)) is
empty
by A22, YELLOW_1:def 4;
a is
Element of
product (Carrier (p | ns))
by YELLOW_1:def 4;
then consider g being
Function such that A25:
(
a = g &
dom g = dom (Carrier (p | ns)) )
and A26:
for
i being
set st
i in dom (Carrier (p | ns)) holds
g . i in (Carrier (p | ns)) . i
by A24, CARD_3:def 5;
reconsider a =
a as
Function by A25;
set y =
a +* (n .--> b);
now set g1 =
a +* (n .--> b);
reconsider g1 =
a +* (n .--> b) as
Function ;
take g1 =
g1;
:: thesis: ( a +* (n .--> b) = g1 & dom g1 = dom (Carrier p) & ( for x being set st x in dom (Carrier p) holds
b2 . b3 in (Carrier p) . b3 ) )thus
a +* (n .--> b) = g1
;
:: thesis: ( dom g1 = dom (Carrier p) & ( for x being set st x in dom (Carrier p) holds
b2 . b3 in (Carrier p) . b3 ) )A27:
dom a = ns
by A25, PARTFUN1:def 4;
A28:
dom (n .--> b) = {n}
by FUNCOP_1:19;
thus dom g1 =
(dom a) \/ (dom (n .--> b))
by FUNCT_4:def 1
.=
n \/ {n}
by A1, A27, FUNCOP_1:19
.=
n + 1
by AFINSQ_1:4
.=
dom (Carrier p)
by PARTFUN1:def 4
;
:: thesis: for x being set st x in dom (Carrier p) holds
b2 . b3 in (Carrier p) . b3let x be
set ;
:: thesis: ( x in dom (Carrier p) implies b1 . b2 in (Carrier p) . b2 )assume A29:
x in dom (Carrier p)
;
:: thesis: b1 . b2 in (Carrier p) . b2A30:
x in n + 1
by A29, PARTFUN1:def 4;
then A31:
x in n \/ {n}
by AFINSQ_1:4;
per cases
( x in n or x in {n} )
by A31, XBOOLE_0:def 3;
suppose A32:
x in n
;
:: thesis: b1 . b2 in (Carrier p) . b2then
x <> n
;
then
not
x in dom (n .--> b)
by A28, TARSKI:def 1;
then A33:
g1 . x = a . x
by FUNCT_4:12;
A34:
x in dom (Carrier (p | ns))
by A1, A32, PARTFUN1:def 4;
consider R being
1-sorted such that A35:
R = (p | ns) . x
and A36:
(Carrier (p | ns)) . x = the
carrier of
R
by A1, A32, PRALG_1:def 13;
consider R2 being
1-sorted such that A37:
R2 = p . x
and A38:
(Carrier p) . x = the
carrier of
R2
by A30, PRALG_1:def 13;
(Carrier (p | ns)) . x = (Carrier p) . x
by A1, A32, A35, A36, A37, A38, FUNCT_1:72;
hence
g1 . x in (Carrier p) . x
by A25, A26, A33, A34;
:: thesis: verum end; 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: S1[x,y]
take
a
;
:: thesis: ex b being Element of pne2 st
( a in ppns2 & x = [a,b] & y = a +* (n .--> b) )
take
b
;
:: thesis: ( a in ppns2 & x = [a,b] & y = a +* (n .--> b) )
thus
a in ppns2
;
:: thesis: ( x = [a,b] & y = a +* (n .--> b) )
thus
x = [a,b]
by MCART_1:23;
:: thesis: y = a +* (n .--> b)
thus
y = a +* (n .--> b)
;
:: thesis: verum
end; consider f being
Function of
CP',
CPP such that A43:
for
x being
Element of
CP' holds
S1[
x,
f . x]
from FUNCT_2:sch 3(A23);
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 f' =
f as
Function of
S,
T ;
take f =
f;
:: thesis: f is isomorphic now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A44:
x1 in dom f
and A45:
x2 in dom f
and A46:
f . x1 = f . x2
;
:: thesis: x1 = x2
x1 is
Element of
[:the carrier of (product (p | ns)),the carrier of (p . ne):]
by A44, YELLOW_3:def 2;
then consider a1 being
Function,
b1 being
Element of
pne2 such that A47:
a1 in ppns2
and A48:
x1 = [a1,b1]
and A49:
f . x1 = a1 +* (n .--> b1)
by A43;
x2 is
Element of
[:the carrier of (product (p | ns)),the carrier of (p . ne):]
by A45, YELLOW_3:def 2;
then consider a2 being
Function,
b2 being
Element of
pne2 such that A50:
a2 in ppns2
and A51:
x2 = [a2,b2]
and A52:
f . x2 = a2 +* (n .--> b2)
by A43;
a1 in product (Carrier (p | ns))
by A47, YELLOW_1:def 4;
then consider g1 being
Function such that A53:
(
a1 = g1 &
dom g1 = dom (Carrier (p | ns)) )
and
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 A50, YELLOW_1:def 4;
then consider g2 being
Function such that A54:
(
a2 = g2 &
dom g2 = dom (Carrier (p | ns)) )
and
for
x being
set st
x in dom (Carrier (p | ns)) holds
g2 . x in (Carrier (p | ns)) . x
by CARD_3:def 5;
A55:
dom (n .--> b1) = {n}
by FUNCOP_1:19;
then A56:
dom (n .--> b1) = dom (n .--> b2)
by FUNCOP_1:19;
A57:
dom a1 = n
by A1, A53, PARTFUN1:def 4;
then A61:
dom a1 misses dom (n .--> b1)
by A57, FUNCOP_1:19;
A62:
dom a2 misses dom (n .--> b2)
by A53, A54, A57, A58, FUNCOP_1:19;
A63:
now let a,
b be
set ;
:: thesis: ( ( [a,b] in a1 implies [a,b] in a2 ) & ( [a,b] in a2 implies [a,b] in a1 ) )hereby :: thesis: ( [a,b] in a2 implies [a,b] in a1 )
assume A64:
[a,b] in a1
;
:: thesis: [a,b] in a2then A65:
(
a in dom a1 &
b = a1 . a )
by FUNCT_1:8;
then A66:
a in (dom a1) \/ (dom (n .--> b1))
by XBOOLE_0:def 3;
then
not
a in dom (n .--> b1)
by A61, A65, XBOOLE_0:5;
then A67:
(a2 +* (n .--> b2)) . a = a1 . a
by A46, A49, A52, A66, FUNCT_4:def 1;
A68:
a in (dom a2) \/ (dom (n .--> b2))
by A53, A54, A65, XBOOLE_0:def 3;
A69:
a in dom a2
by A53, A54, A64, FUNCT_1:8;
then
not
a in dom (n .--> b2)
by A62, A68, XBOOLE_0:5;
then
b = a2 . a
by A65, A67, A68, FUNCT_4:def 1;
hence
[a,b] in a2
by A69, FUNCT_1:8;
:: thesis: verum
end; assume A70:
[a,b] in a2
;
:: thesis: [a,b] in a1then A71:
(
a in dom a2 &
b = a2 . a )
by FUNCT_1:8;
then A72:
a in (dom a2) \/ (dom (n .--> b2))
by XBOOLE_0:def 3;
then
not
a in dom (n .--> b2)
by A62, A71, XBOOLE_0:5;
then A73:
(a1 +* (n .--> b1)) . a = a2 . a
by A46, A49, A52, A72, FUNCT_4:def 1;
A74:
a in (dom a1) \/ (dom (n .--> b1))
by A53, A54, A71, XBOOLE_0:def 3;
A75:
a in dom a1
by A53, A54, A70, FUNCT_1:8;
then
not
a in dom (n .--> b1)
by A61, A74, XBOOLE_0:5;
then
b = a1 . a
by A71, A73, A74, FUNCT_4:def 1;
hence
[a,b] in a1
by A75, FUNCT_1:8;
:: thesis: verum end; A76:
n in dom (n .--> b1)
by A55, TARSKI:def 1;
then A77:
n in (dom a1) \/ (dom (n .--> b1))
by XBOOLE_0:def 3;
A78:
n in dom (n .--> b2)
by A55, A56, 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 A46, A49, A52, A78, FUNCT_4:def 1
.=
b2
by FUNCOP_1:87
;
then b2 =
(n .--> b1) . n
by A76, A77, FUNCT_4:def 1
.=
b1
by FUNCOP_1:87
;
hence
x1 = x2
by A48, A51, A63, RELAT_1:def 2;
:: thesis: verum end; then A79:
f is
one-to-one
by FUNCT_1:def 8;
now let y be
set ;
:: thesis: ( ( y in rng f implies y in the carrier of (product p) ) & ( y in the carrier of (product p) implies y in rng f ) )thus
(
y in rng f implies
y in the
carrier of
(product p) )
;
:: thesis: ( y in the carrier of (product p) implies y in rng f )assume
y in the
carrier of
(product p)
;
:: thesis: y in rng fthen
y in product (Carrier p)
by YELLOW_1:def 4;
then consider g being
Function such that A80:
y = g
and A81:
dom g = dom (Carrier p)
and A82:
for
x being
set st
x in dom (Carrier p) holds
g . x in (Carrier p) . x
by CARD_3:def 5;
A83:
dom (Carrier p) = n + 1
by PARTFUN1:def 4;
A84:
n + 1
= { i where i is Element of NAT : i < n + 1 }
by AXIOMS:30;
X:
n in NAT
by ORDINAL1:def 13;
n < n + 1
by NAT_1:13;
then A85:
n in n + 1
by A84, X;
set a =
g | n;
set b =
g . n;
set x =
[(g | n),(g . n)];
A86:
dom (Carrier (p | ns)) = ns
by PARTFUN1:def 4;
A87:
dom (g | n) =
(dom g) /\ n
by RELAT_1:90
.=
(n + 1) /\ n
by A81, PARTFUN1:def 4
;
then A88:
dom (g | n) = n
by Th2, XBOOLE_1:28;
A89:
dom (g | n) = dom (Carrier (p | ns))
by A1, A86, A87, XBOOLE_1:28;
now let x be
set ;
:: thesis: ( x in dom (Carrier (p | ns)) implies (g | n) . x in (Carrier (p | ns)) . x )assume
x in dom (Carrier (p | ns))
;
:: thesis: (g | n) . x in (Carrier (p | ns)) . xthen A90:
x in n
by A1, PARTFUN1:def 4;
A91:
n c= n + 1
by Th2;
A92:
(g | n) . x = g . x
by A90, FUNCT_1:72;
A93:
g . x in (Carrier p) . x
by A82, A83, A90, A91;
consider R1 being
1-sorted such that A94:
(
R1 = p . x &
(Carrier p) . x = the
carrier of
R1 )
by A90, A91, PRALG_1:def 13;
consider R2 being
1-sorted such that A95:
(
R2 = (p | ns) . x &
(Carrier (p | ns)) . x = the
carrier of
R2 )
by A1, A90, PRALG_1:def 13;
thus
(g | n) . x in (Carrier (p | ns)) . x
by A1, A90, A92, A93, A94, A95, FUNCT_1:72;
:: thesis: verum end; then
g | n in product (Carrier (p | ns))
by A89, CARD_3:18;
then A96:
g | n in the
carrier of
(product (p | ns))
by YELLOW_1:def 4;
consider R1 being
1-sorted such that A97:
(
R1 = p . n &
(Carrier p) . n = the
carrier of
R1 )
by A85, PRALG_1:def 13;
A98:
g . n in the
carrier of
(p . ne)
by A2, A82, A83, A97;
then
[(g | n),(g . n)] in [:the carrier of (product (p | ns)),the carrier of (p . ne):]
by A96, ZFMISC_1:106;
then A99:
[(g | n),(g . n)] in dom f
by FUNCT_2:def 1;
[(g | n),(g . n)] is
Element of
CP'
by A96, A98, ZFMISC_1:106;
then consider ta being
Function,
tb being
Element of
pne2 such that
ta in ppns2
and A100:
[(g | n),(g . n)] = [ta,tb]
and A101:
f . [(g | n),(g . n)] = ta +* (n .--> tb)
by A43;
A102:
(
ta = g | n &
tb = g . n )
by A100, ZFMISC_1:33;
now let i,
j be
set ;
:: thesis: ( ( [i,j] in (g | n) +* (n .--> (g . n)) implies [i,j] in g ) & ( [i,j] in g implies [b1,b2] in (g | n) +* (n .--> (g . n)) ) )hereby :: thesis: ( [i,j] in g implies [b1,b2] in (g | n) +* (n .--> (g . n)) )
assume A103:
[i,j] in (g | n) +* (n .--> (g . n))
;
:: thesis: [i,j] in gthen
i in dom ((g | n) +* (n .--> (g . n)))
by FUNCT_1:8;
then A104:
i in (dom (g | n)) \/ (dom (n .--> (g . n)))
by FUNCT_4:def 1;
then A105:
i in n \/ {n}
by A88, FUNCOP_1:19;
A106:
((g | n) +* (n .--> (g . n))) . i = j
by A103, FUNCT_1:8;
per cases
( i in dom (n .--> (g . n)) or not i in dom (n .--> (g . n)) )
;
suppose A107:
i in dom (n .--> (g . n))
;
:: thesis: [i,j] in gthen
i in {n}
by FUNCOP_1:19;
then A108:
i = n
by TARSKI:def 1;
((g | n) +* (n .--> (g . n))) . i =
(n .--> (g . n)) . i
by A104, A107, FUNCT_4:def 1
.=
g . n
by A108, FUNCOP_1:87
;
then A109:
g . i = j
by A103, A108, FUNCT_1:8;
i in dom g
by A81, A83, A105, AFINSQ_1:4;
hence
[i,j] in g
by A109, FUNCT_1:8;
:: thesis: verum end; suppose A110:
not
i in dom (n .--> (g . n))
;
:: thesis: [i,j] in gthen
not
i in {n}
by FUNCOP_1:19;
then A111:
i in n
by A105, XBOOLE_0:def 3;
((g | n) +* (n .--> (g . n))) . i = (g | n) . i
by A104, A110, FUNCT_4:def 1;
then A112:
g . i = j
by A106, A111, FUNCT_1:72;
i in dom g
by A81, A83, A105, AFINSQ_1:4;
hence
[i,j] in g
by A112, FUNCT_1:8;
:: thesis: verum end;
end; assume A113:
[i,j] in g
;
:: thesis: [b1,b2] in (g | n) +* (n .--> (g . n))then A114:
i in n + 1
by A81, A83, FUNCT_1:8;
then A115:
i in n \/ {n}
by AFINSQ_1:4;
dom ((g | n) +* (n .--> (g . n))) =
(dom (g | n)) \/ (dom (n .--> (g . n)))
by FUNCT_4:def 1
.=
n \/ {n}
by A88, FUNCOP_1:19
;
then A116:
i in dom ((g | n) +* (n .--> (g . n)))
by A114, AFINSQ_1:4;
then A117:
i in (dom (g | n)) \/ (dom (n .--> (g . n)))
by FUNCT_4:def 1;
end; then
f . [(g | n),(g . n)] = y
by A80, A101, A102, RELAT_1:def 2;
hence
y in rng f
by A99, FUNCT_1:def 5;
:: thesis: verum end; then A122:
rng f = the
carrier of
(product p)
by TARSKI:2;
now let x,
y be
Element of
S;
:: thesis: ( ( x <= y implies f' . x <= f' . y ) & ( f' . x <= f' . y implies x <= y ) )A123:
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 A124:
xa in ppns2
and A125:
x = [xa,xb]
and A126:
f . x = xa +* (n .--> xb)
by A43;
dom f = CP'
by FUNCT_2:def 1;
then
f . x in the
carrier of
(product p)
by A122, A123, FUNCT_1:def 5;
then A127:
f' . 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 A128:
ya in ppns2
and A129:
y = [ya,yb]
and A130:
f . y = ya +* (n .--> yb)
by A43;
A131:
[x,y] `1 = x
by MCART_1:def 1;
A132:
[x,y] `2 = y
by MCART_1:def 2;
A133:
x `1 = xa
by A125, MCART_1:def 1;
A134:
x `2 = xb
by A125, MCART_1:def 2;
A135:
xa in product (Carrier (p | ns))
by A124, YELLOW_1:def 4;
then consider gx being
Function such that A136:
(
xa = gx &
dom gx = dom (Carrier (p | ns)) )
and A137:
for
x being
set st
x in dom (Carrier (p | ns)) holds
gx . x in (Carrier (p | ns)) . x
by CARD_3:def 5;
A138:
dom xa = n
by A1, A136, PARTFUN1:def 4;
then A139:
(dom xa) \/ (dom (n .--> xb)) = n \/ {n}
by FUNCOP_1:19;
ya in product (Carrier (p | ns))
by A128, YELLOW_1:def 4;
then consider gy being
Function such that A140:
(
ya = gy &
dom gy = dom (Carrier (p | ns)) )
and A141:
for
x being
set st
x in dom (Carrier (p | ns)) holds
gy . x in (Carrier (p | ns)) . x
by CARD_3:def 5;
A142:
dom ya = n
by A1, A140, PARTFUN1:def 4;
then A143:
(dom ya) \/ (dom (n .--> yb)) = n \/ {n}
by FUNCOP_1:19;
reconsider xa' =
xa as
Element of
(product (p | ns)) by A124;
reconsider ya' =
ya as
Element of
(product (p | ns)) by A128;
hereby :: thesis: ( f' . x <= f' . y implies x <= y )
assume
x <= y
;
:: thesis: f' . x <= f' . ythen
[x,y] in the
InternalRel of
S
by ORDERS_2:def 9;
then
[x,y] in ["the InternalRel of (product (p | ns)),the InternalRel of (p . ne)"]
by YELLOW_3:def 2;
then A144:
(
[(([x,y] `1 ) `1 ),(([x,y] `2 ) `1 )] in the
InternalRel of
(product (p | ns)) &
[(([x,y] `1 ) `2 ),(([x,y] `2 ) `2 )] in the
InternalRel of
(p . ne) & ex
a,
b being
set st
[x,y] = [a,b] & ex
c,
d being
set st
[x,y] `1 = [c,d] & ex
e,
f being
set st
[x,y] `2 = [e,f] )
by YELLOW_3:10;
then A145:
[xa,ya] in the
InternalRel of
(product (p | ns))
by A129, A131, A132, A133, MCART_1:def 1;
A146:
xa in product (Carrier (p | ns))
by A124, YELLOW_1:def 4;
xa' <= ya'
by A145, ORDERS_2:def 9;
then consider ffx,
ggx being
Function such that A147:
(
ffx = xa &
ggx = ya )
and A148:
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, A146, YELLOW_1:def 4;
A149:
[xb,yb] in the
InternalRel of
(p . ne)
by A129, A131, A132, A134, A144, MCART_1:def 2;
reconsider xb' =
xb as
Element of
(p . ne) ;
reconsider yb' =
yb as
Element of
(p . ne) ;
A150:
xb' <= yb'
by A149, ORDERS_2:def 9;
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: ex g1 being Function st
( xa +* (n .--> xb) = 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 = (xa +* (n .--> xb)) . i & yi = g1 . i & xi <= yi ) ) )
take
ya +* (n .--> yb)
;
:: thesis: ( xa +* (n .--> xb) = f . x & ya +* (n .--> yb) = 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 = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi ) ) )
thus
xa +* (n .--> xb) = f . x
by A126;
:: thesis: ( ya +* (n .--> yb) = 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 = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi ) ) )
thus
ya +* (n .--> yb) = f . y
by A130;
:: thesis: 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 = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
let i be
set ;
:: thesis: ( i in n + 1 implies ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi ) )
assume A151:
i in n + 1
;
:: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
A152:
i in n \/ {n}
by A151, AFINSQ_1:4;
set R =
p . i;
set xi =
(xa +* (n .--> xb)) . i;
set yi =
(ya +* (n .--> yb)) . i;
i in dom p
by A151, PARTFUN1:def 4;
then
p . i in rng p
by FUNCT_1:def 5;
then reconsider R =
p . i as
RelStr by YELLOW_1:def 3;
A153:
i in (dom xa) \/ (dom (n .--> xb))
by A139, A151, AFINSQ_1:4;
now per cases
( i in dom (n .--> xb) or not i in dom (n .--> xb) )
;
suppose A156:
not
i in dom (n .--> xb)
;
:: thesis: (xa +* (n .--> xb)) . i is Element of Rthen A157:
not
i in {n}
by FUNCOP_1:19;
then A158:
i in n
by A152, XBOOLE_0:def 3;
A159:
i in dom (Carrier (p | ns))
by A3, A152, A157, XBOOLE_0:def 3;
(xa +* (n .--> xb)) . i = xa . i
by A153, A156, FUNCT_4:def 1;
then A160:
(xa +* (n .--> xb)) . i in (Carrier (p | ns)) . i
by A136, A137, A159;
consider R2 being
1-sorted such that A161:
(
R2 = (p | ns) . i &
(Carrier (p | ns)) . i = the
carrier of
R2 )
by A1, A158, PRALG_1:def 13;
thus
(xa +* (n .--> xb)) . i is
Element of
R
by A1, A158, A160, A161, FUNCT_1:72;
:: thesis: verum end;
then reconsider xi =
(xa +* (n .--> xb)) . i as
Element of
R ;
A162:
i in (dom ya) \/ (dom (n .--> yb))
by A143, A151, AFINSQ_1:4;
now per cases
( i in dom (n .--> yb) or not i in dom (n .--> yb) )
;
suppose A165:
not
i in dom (n .--> yb)
;
:: thesis: (ya +* (n .--> yb)) . i is Element of Rthen A166:
not
i in {n}
by FUNCOP_1:19;
then A167:
i in n
by A152, XBOOLE_0:def 3;
A168:
i in dom (Carrier (p | ns))
by A3, A152, A166, XBOOLE_0:def 3;
(ya +* (n .--> yb)) . i = ya . i
by A162, A165, FUNCT_4:def 1;
then A169:
(ya +* (n .--> yb)) . i in (Carrier (p | ns)) . i
by A140, A141, A168;
consider R2 being
1-sorted such that A170:
(
R2 = (p | ns) . i &
(Carrier (p | ns)) . i = the
carrier of
R2 )
by A1, A167, PRALG_1:def 13;
thus
(ya +* (n .--> yb)) . i is
Element of
R
by A1, A167, A169, A170, FUNCT_1:72;
:: thesis: verum end;
then reconsider yi =
(ya +* (n .--> yb)) . i as
Element of
R ;
take
R
;
:: thesis: ex xi, yi being Element of R st
( R = p . i & xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
take
xi
;
:: thesis: ex yi being Element of R st
( R = p . i & xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
take
yi
;
:: thesis: ( R = p . i & xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
thus
R = p . i
;
:: thesis: ( xi = (xa +* (n .--> xb)) . i & yi = (ya +* (n .--> yb)) . i & xi <= yi )
thus
xi = (xa +* (n .--> xb)) . i
;
:: thesis: ( yi = (ya +* (n .--> yb)) . i & xi <= yi )
thus
yi = (ya +* (n .--> yb)) . i
;
:: thesis: xi <= yi
per cases
( i in n or i in {n} )
by A152, XBOOLE_0:def 3;
suppose A171:
i in n
;
:: thesis: xi <= yiA172:
not
i in {n}
then A173:
not
i in dom (n .--> xb)
by FUNCOP_1:19;
not
i in dom (n .--> yb)
by A172, FUNCOP_1:19;
then A174:
yi = ya . i
by A162, FUNCT_4:def 1;
consider RR being
RelStr ,
xxi,
yyi being
Element of
RR such that A175:
RR = (p | ns) . i
and A176:
(
xxi = ffx . i &
yyi = ggx . i )
and A177:
xxi <= yyi
by A148, A171;
RR = R
by A1, A171, A175, FUNCT_1:72;
hence
xi <= yi
by A147, A153, A173, A174, A176, A177, FUNCT_4:def 1;
:: thesis: verum end; suppose A178:
i in {n}
;
:: thesis: xi <= yithen A179:
i = n
by TARSKI:def 1;
A180:
i in dom (n .--> xb)
by A178, FUNCOP_1:19;
A181:
i in dom (n .--> yb)
by A178, FUNCOP_1:19;
A182:
xi =
(n .--> xb) . i
by A153, A180, FUNCT_4:def 1
.=
xb
by A179, FUNCOP_1:87
;
yi =
(n .--> yb) . i
by A162, A181, FUNCT_4:def 1
.=
yb
by A179, FUNCOP_1:87
;
hence
xi <= yi
by A2, A150, A178, A182, TARSKI:def 1;
:: thesis: verum end;
end; hence
f' . x <= f' . y
by A127, YELLOW_1:def 4;
:: thesis: verum
end; assume
f' . x <= f' . y
;
:: thesis: x <= ythen consider f1,
g1 being
Function such that A183:
f1 = f . x
and A184:
g1 = f . y
and A185:
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 A127, YELLOW_1:def 4;
now set f2 =
xa';
set g2 =
ya';
reconsider f2 =
xa',
g2 =
ya' as
Function ;
take f2 =
f2;
:: thesis: ex g2 being Function st
( f2 = xa' & g2 = ya' & ( for i being set st i in ns holds
ex R being RelStr ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )take g2 =
g2;
:: thesis: ( f2 = xa' & g2 = ya' & ( for i being set st i in ns holds
ex R being RelStr ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )thus
(
f2 = xa' &
g2 = ya' )
;
:: thesis: for i being set st i in ns holds
ex R being RelStr ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi )let i be
set ;
:: thesis: ( i in ns implies ex R being RelStr ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) )assume A186:
i in ns
;
:: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi )A187:
not
i in {n}
then A188:
not
i in dom (n .--> yb)
by FUNCOP_1:19;
A189:
not
i in dom (n .--> xb)
by A187, FUNCOP_1:19;
set R =
(p | ns) . i;
i in dom (p | ns)
by A186, PARTFUN1:def 4;
then
(p | ns) . i in rng (p | ns)
by FUNCT_1:def 5;
then reconsider R =
(p | ns) . i as
RelStr by YELLOW_1:def 3;
take R =
R;
:: thesis: ex xi, yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi )set xi =
xa . i;
set yi =
ya . i;
A190:
i in (dom xa) \/ (dom (n .--> xb))
by A1, A138, A186, XBOOLE_0:def 3;
A191:
i in dom (Carrier (p | ns))
by A186, PARTFUN1:def 4;
consider R2 being
1-sorted such that A192:
(
R2 = (p | ns) . i &
(Carrier (p | ns)) . i = the
carrier of
R2 )
by A186, PRALG_1:def 13;
reconsider xi =
xa . i as
Element of
R by A136, A137, A191, A192;
A193:
i in (dom ya) \/ (dom (n .--> yb))
by A1, A142, A186, XBOOLE_0:def 3;
consider R2 being
1-sorted such that A194:
(
R2 = (p | ns) . i &
(Carrier (p | ns)) . i = the
carrier of
R2 )
by A186, PRALG_1:def 13;
reconsider yi =
ya . i as
Element of
R by A140, A141, A191, A194;
take xi =
xi;
:: thesis: ex yi being Element of R st
( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi )take yi =
yi;
:: thesis: ( R = (p | ns) . i & xi = f2 . i & yi = g2 . i & xi <= yi )thus
(
R = (p | ns) . i &
xi = f2 . i &
yi = g2 . i )
;
:: thesis: xi <= yiconsider R2 being
RelStr ,
xi2,
yi2 being
Element of
R2 such that A195:
R2 = p . i
and A196:
xi2 = f1 . i
and A197:
yi2 = g1 . i
and A198:
xi2 <= yi2
by A185, A186;
A199:
R2 = R
by A186, A195, FUNCT_1:72;
(xa +* (n .--> xb)) . i = xi
by A189, A190, FUNCT_4:def 1;
hence
xi <= yi
by A126, A130, A183, A184, A188, A193, A196, A197, A198, A199, FUNCT_4:def 1;
:: thesis: verum end; then
xa' <= ya'
by A135, YELLOW_1:def 4;
then
[xa,ya] in the
InternalRel of
(product (p | ns))
by ORDERS_2:def 9;
then A200:
[(([x,y] `1 ) `1 ),(([x,y] `2 ) `1 )] in the
InternalRel of
(product (p | ns))
by A129, A131, A132, A133, MCART_1:def 1;
consider Rn being
RelStr ,
xni,
yni being
Element of
Rn such that A201:
Rn = p . ne
and A202:
xni = f1 . n
and A203:
yni = g1 . n
and A204:
xni <= yni
by A2, A185;
A205:
[xni,yni] in the
InternalRel of
(p . ne)
by A201, A204, ORDERS_2:def 9;
dom (n .--> xb) = {n}
by FUNCOP_1:19;
then A206:
n in dom (n .--> xb)
by TARSKI:def 1;
then
n in (dom xa) \/ (dom (n .--> xb))
by XBOOLE_0:def 3;
then A207:
(xa +* (n .--> xb)) . n =
(n .--> xb) . n
by A206, FUNCT_4:def 1
.=
xb
by FUNCOP_1:87
;
dom (n .--> yb) = {n}
by FUNCOP_1:19;
then A208:
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 A208, FUNCT_4:def 1
.=
yb
by FUNCOP_1:87
;
then A209:
[(([x,y] `1 ) `2 ),(([x,y] `2 ) `2 )] in the
InternalRel of
(p . ne)
by A126, A129, A130, A131, A132, A134, A183, A184, A202, A203, A205, A207, MCART_1:def 2;
(
[x,y] `1 = [xa,xb] &
[x,y] `2 = [ya,yb] )
by A125, A129, MCART_1:def 1, MCART_1:def 2;
then
[x,y] in ["the InternalRel of (product (p | ns)),the InternalRel of (p . ne)"]
by A200, A209, YELLOW_3:10;
then
[x,y] in the
InternalRel of
S
by YELLOW_3:def 2;
hence
x <= y
by ORDERS_2:def 9;
:: thesis: verum end; hence
f is
isomorphic
by A79, A122, WAYBEL_0:66;
:: thesis: verum hence
[:(product (p | ns)),(p . ne):],
product p are_isomorphic
by WAYBEL_1:def 8;
:: thesis: verum end;