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

proof

A23: dom M1 = the carrier of (MonSet L) by FUNCT_2:def 1;
A24: 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 A25: s in the carrier of (MonSet L) ; :: thesis: M1 . s = M2 . s
then consider AR1 being auxiliary Relation of L such that
A26: ( AR1 = M1 . s & ( for x, y being set holds
( [x,y] in AR1 iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) by A21;
consider AR2 being auxiliary Relation of L such that
A27: ( AR2 = M2 . s & ( for x, y being set holds
( [x,y] in AR2 iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) by A22, A25;
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 consider x', y' being Element of L, s' being Function of L,(InclPoset (Ids L)) such that
A28: ( x' = x & y' = y & s' = s & x' in s' . y' ) by A26;
thus [x,y] in AR2 by A27, A28; :: thesis: verum

end;

assume [x,y] in AR2 ; :: thesis: [x,y] in AR1
then consider x', y' being Element of L, s' being Function of L,(InclPoset (Ids L)) such that
A29: ( x' = x & y' = y & s' = s & x' in s' . y' ) by A27;
thus [x,y] in AR1 by A26, A29; :: thesis: verum

end;

hence M1 . s = M2 . s by A26, A27; :: thesis: verum

end;

hence M1 = M2 by A23, A24, FUNCT_1:9; :: thesis: verum

end;

hence M1 = M2 ; :: thesis: verum