let M1, M2 be Function of (MonSet L),(InclPoset (Aux L)); :: thesis: ( ( 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 ) ) ) ) ; :: thesis: ( 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 ) ) ) ) ; :: thesis: 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 ; :: thesis: ( s in the carrier of (MonSet L) implies M1 . s = M2 . s )
assume A39: s in the carrier of (MonSet L) ; :: thesis: 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 ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in AR1 or [x,y] in AR2 ) & ( not [x,y] in AR2 or [x,y] in AR1 ) )
hereby :: thesis: ( not [x,y] in AR2 or [x,y] in AR1 )
assume [x,y] in AR1 ; :: thesis: [x,y] in AR2
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 A41;
hence [x,y] in AR2 by A43; :: thesis: verum
end;
assume [x,y] in AR2 ; :: thesis: [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; :: thesis: verum
end;
hence M1 . s = M2 . s by A40, A42; :: thesis: verum
end;
hence M1 = M2 by A37, A38, FUNCT_1:2; :: thesis: verum