let M1, M2 be Function of (MonSet L),(InclPoset (Aux L)); ( ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M1 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M2 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) implies M1 = M2 )
assume A35:
for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M1 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
; ( ex s being object st
( s in the carrier of (MonSet L) & ( for AR being auxiliary Relation of L holds
( not AR = M2 . s or ex x, y being object st
( ( [x,y] in AR implies ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) implies ( ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) & not [x,y] in AR ) ) ) ) ) or M1 = M2 )
assume A36:
for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M2 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
; M1 = M2
A37:
dom M1 = the carrier of (MonSet L)
by FUNCT_2:def 1;
A38:
dom M2 = the carrier of (MonSet L)
by FUNCT_2:def 1;
for s being object st s in the carrier of (MonSet L) holds
M1 . s = M2 . s
proof
let s be
object ;
( s in the carrier of (MonSet L) implies M1 . s = M2 . s )
assume A39:
s in the
carrier of
(MonSet L)
;
M1 . s = M2 . s
then consider AR1 being
auxiliary Relation of
L such that A40:
AR1 = M1 . s
and A41:
for
x,
y being
object holds
(
[x,y] in AR1 iff ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = x &
y9 = y &
s9 = s &
x9 in s9 . y9 ) )
by A35;
consider AR2 being
auxiliary Relation of
L such that A42:
AR2 = M2 . s
and A43:
for
x,
y being
object holds
(
[x,y] in AR2 iff ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = x &
y9 = y &
s9 = s &
x9 in s9 . y9 ) )
by A36, A39;
AR1 = AR2
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in AR1 or [x,y] in AR2 ) & ( not [x,y] in AR2 or [x,y] in AR1 ) )
hereby ( not [x,y] in AR2 or [x,y] in AR1 )
end;
assume
[x,y] in AR2
;
[x,y] in AR1
then
ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = x &
y9 = y &
s9 = s &
x9 in s9 . y9 )
by A43;
hence
[x,y] in AR1
by A41;
verum
end;
hence
M1 . s = M2 . s
by A40, A42;
verum
end;
hence
M1 = M2
by A37, A38, FUNCT_1:2; verum