let M1, M2 be Function of (MonSet L),(InclPoset (Aux L)); :: thesis: ( ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = M1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ) & ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = M2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ) implies M1 = M2 )
assume A35: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = M1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ; :: thesis: ( ex s being set st
( s in the carrier of (MonSet L) & ( for AR being auxiliary Relation of holds
( not AR = M2 . s or ex x, y being set st
( ( [x,y] in AR implies ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) implies ( ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) & not [x,y] in AR ) ) ) ) ) or M1 = M2 )
assume A36: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = M2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ; :: 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 set st s in the carrier of (MonSet L) holds
M1 . s = M2 . s

proof

let s be set ; :: 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 such that
A40: AR1 = M1 . s and
A41: for x, y being set holds
( [x,y] in AR1 iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) by A35;
consider AR2 being auxiliary Relation of such that
A42: AR2 = M2 . s and
A43: for x, y being set holds
( [x,y] in AR2 iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) by A36, A39;
AR1 = AR2

proof

let x, y be set ; :: 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 x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) by A41;
hence [x,y] in AR2 by A43; :: thesis: verum

end;

assume [x,y] in AR2 ; :: thesis: [x,y] in AR1
then ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) 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:9; :: thesis: verum