let X be set ; for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds
L |^ X = S |^ X
let L, S be non empty RelStr ; ( RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) implies L |^ X = S |^ X )
assume A1:
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #)
; L |^ X = S |^ X
reconsider tXL = X --> L as RelStr-yielding ManySortedSet of X ;
reconsider tXS = X --> S as RelStr-yielding ManySortedSet of X ;
A2:
for x being object st x in dom (Carrier tXS) holds
(Carrier tXS) . x = (Carrier tXL) . x
A5: dom (Carrier tXS) =
X
by PARTFUN1:def 2
.=
dom (Carrier tXL)
by PARTFUN1:def 2
;
A6: the carrier of (S |^ X) =
the carrier of (product tXS)
by YELLOW_1:def 5
.=
product (Carrier tXS)
by YELLOW_1:def 4
.=
product (Carrier tXL)
by A5, A2, FUNCT_1:2
.=
the carrier of (product tXL)
by YELLOW_1:def 4
.=
the carrier of (L |^ X)
by YELLOW_1:def 5
;
A7:
the InternalRel of (L |^ X) c= the InternalRel of (S |^ X)
proof
reconsider tXS =
X --> S as
RelStr-yielding ManySortedSet of
X ;
reconsider tXL =
X --> L as
RelStr-yielding ManySortedSet of
X ;
let x be
object ;
TARSKI:def 3 ( not x in the InternalRel of (L |^ X) or x in the InternalRel of (S |^ X) )
assume A8:
x in the
InternalRel of
(L |^ X)
;
x in the InternalRel of (S |^ X)
then consider a,
b being
object such that A9:
x = [a,b]
and A10:
a in the
carrier of
(L |^ X)
and A11:
b in the
carrier of
(L |^ X)
by RELSET_1:2;
reconsider a =
a,
b =
b as
Element of
(L |^ X) by A10, A11;
A12:
L |^ X = product tXL
by YELLOW_1:def 5;
then A13:
the
carrier of
(L |^ X) = product (Carrier tXL)
by YELLOW_1:def 4;
a <= b
by A8, A9, ORDERS_2:def 5;
then consider f,
g being
Function such that A14:
f = a
and A15:
g = b
and A16:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = tXL . i &
xi = f . i &
yi = g . i &
xi <= yi )
by A12, A13, YELLOW_1:def 4;
reconsider a1 =
a,
b1 =
b as
Element of
(S |^ X) by A6;
A17:
ex
f,
g being
Function st
(
f = a1 &
g = b1 & ( for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = tXS . i &
xi = f . i &
yi = g . i &
xi <= yi ) ) )
proof
take
f
;
ex g being Function st
( f = a1 & g = b1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take
g
;
( f = a1 & g = b1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus
(
f = a1 &
g = b1 )
by A14, A15;
for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXS . i & xi = f . i & yi = g . i & xi <= yi )
let i be
object ;
( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A18:
i in X
;
ex R being RelStr ex xi, yi being Element of R st
( R = tXS . i & xi = f . i & yi = g . i & xi <= yi )
then consider R being
RelStr ,
xi,
yi being
Element of
R such that A19:
R = tXL . i
and A20:
xi = f . i
and A21:
yi = g . i
and A22:
xi <= yi
by A16;
take R1 =
S;
ex xi, yi being Element of R1 st
( R1 = tXS . i & xi = f . i & yi = g . i & xi <= yi )
reconsider xi1 =
xi,
yi1 =
yi as
Element of
R1 by A1, A18, A19, FUNCOP_1:7;
take
xi1
;
ex yi being Element of R1 st
( R1 = tXS . i & xi1 = f . i & yi = g . i & xi1 <= yi )
take
yi1
;
( R1 = tXS . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 )
thus
R1 = tXS . i
by A18, FUNCOP_1:7;
( xi1 = f . i & yi1 = g . i & xi1 <= yi1 )
thus
(
xi1 = f . i &
yi1 = g . i )
by A20, A21;
xi1 <= yi1
the
InternalRel of
R = the
InternalRel of
L
by A18, A19, FUNCOP_1:7;
then
[xi1,yi1] in the
InternalRel of
R1
by A1, A22, ORDERS_2:def 5;
hence
xi1 <= yi1
by ORDERS_2:def 5;
verum
end;
A23:
S |^ X = product tXS
by YELLOW_1:def 5;
then
the
carrier of
(S |^ X) = product (Carrier tXS)
by YELLOW_1:def 4;
then
a1 <= b1
by A17, A23, YELLOW_1:def 4;
hence
x in the
InternalRel of
(S |^ X)
by A9, ORDERS_2:def 5;
verum
end;
the InternalRel of (S |^ X) c= the InternalRel of (L |^ X)
proof
reconsider tXL =
X --> L as
RelStr-yielding ManySortedSet of
X ;
reconsider tXS =
X --> S as
RelStr-yielding ManySortedSet of
X ;
let x be
object ;
TARSKI:def 3 ( not x in the InternalRel of (S |^ X) or x in the InternalRel of (L |^ X) )
assume A24:
x in the
InternalRel of
(S |^ X)
;
x in the InternalRel of (L |^ X)
then consider a,
b being
object such that A25:
x = [a,b]
and A26:
a in the
carrier of
(S |^ X)
and A27:
b in the
carrier of
(S |^ X)
by RELSET_1:2;
reconsider a =
a,
b =
b as
Element of
(S |^ X) by A26, A27;
A28:
S |^ X = product tXS
by YELLOW_1:def 5;
then A29:
the
carrier of
(S |^ X) = product (Carrier tXS)
by YELLOW_1:def 4;
a <= b
by A24, A25, ORDERS_2:def 5;
then consider f,
g being
Function such that A30:
f = a
and A31:
g = b
and A32:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = tXS . i &
xi = f . i &
yi = g . i &
xi <= yi )
by A28, A29, YELLOW_1:def 4;
reconsider a1 =
a,
b1 =
b as
Element of
(L |^ X) by A6;
A33:
ex
f,
g being
Function st
(
f = a1 &
g = b1 & ( for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = tXL . i &
xi = f . i &
yi = g . i &
xi <= yi ) ) )
proof
take
f
;
ex g being Function st
( f = a1 & g = b1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take
g
;
( f = a1 & g = b1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus
(
f = a1 &
g = b1 )
by A30, A31;
for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = tXL . i & xi = f . i & yi = g . i & xi <= yi )
let i be
object ;
( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A34:
i in X
;
ex R being RelStr ex xi, yi being Element of R st
( R = tXL . i & xi = f . i & yi = g . i & xi <= yi )
then consider R being
RelStr ,
xi,
yi being
Element of
R such that A35:
R = tXS . i
and A36:
xi = f . i
and A37:
yi = g . i
and A38:
xi <= yi
by A32;
take R1 =
L;
ex xi, yi being Element of R1 st
( R1 = tXL . i & xi = f . i & yi = g . i & xi <= yi )
reconsider xi1 =
xi,
yi1 =
yi as
Element of
R1 by A1, A34, A35, FUNCOP_1:7;
take
xi1
;
ex yi being Element of R1 st
( R1 = tXL . i & xi1 = f . i & yi = g . i & xi1 <= yi )
take
yi1
;
( R1 = tXL . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 )
thus
R1 = tXL . i
by A34, FUNCOP_1:7;
( xi1 = f . i & yi1 = g . i & xi1 <= yi1 )
thus
(
xi1 = f . i &
yi1 = g . i )
by A36, A37;
xi1 <= yi1
the
InternalRel of
R = the
InternalRel of
S
by A34, A35, FUNCOP_1:7;
then
[xi1,yi1] in the
InternalRel of
R1
by A1, A38, ORDERS_2:def 5;
hence
xi1 <= yi1
by ORDERS_2:def 5;
verum
end;
A39:
L |^ X = product tXL
by YELLOW_1:def 5;
then
the
carrier of
(L |^ X) = product (Carrier tXL)
by YELLOW_1:def 4;
then
a1 <= b1
by A33, A39, YELLOW_1:def 4;
hence
x in the
InternalRel of
(L |^ X)
by A25, ORDERS_2:def 5;
verum
end;
hence
L |^ X = S |^ X
by A7, A6, XBOOLE_0:def 10; verum