set P = InclPoset (Ids S);

let f, g be Function of (InclPoset (Ids S)),(InclPoset (Ids L)); :: thesis: ( ( for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J ) ) & ( for I being Ideal of S ex J being Subset of L st

( I = J & g . I = downarrow J ) ) implies f = g )

assume that

A6: for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J ) and

A7: for I being Ideal of S ex J being Subset of L st

( I = J & g . I = downarrow J ) ; :: thesis: f = g

A8: the carrier of (InclPoset (Ids S)) = the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def 1

.= Ids S ;

dom f = the carrier of (InclPoset (Ids S)) by FUNCT_2:def 1;

hence f = g by A11, A9, FUNCT_1:2; :: thesis: verum

let f, g be Function of (InclPoset (Ids S)),(InclPoset (Ids L)); :: thesis: ( ( for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J ) ) & ( for I being Ideal of S ex J being Subset of L st

( I = J & g . I = downarrow J ) ) implies f = g )

assume that

A6: for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J ) and

A7: for I being Ideal of S ex J being Subset of L st

( I = J & g . I = downarrow J ) ; :: thesis: f = g

A8: the carrier of (InclPoset (Ids S)) = the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def 1

.= Ids S ;

A9: now :: thesis: for x being object st x in the carrier of (InclPoset (Ids S)) holds

f . x = g . x

A11:
dom g = the carrier of (InclPoset (Ids S))
by FUNCT_2:def 1;f . x = g . x

let x be object ; :: thesis: ( x in the carrier of (InclPoset (Ids S)) implies f . x = g . x )

assume x in the carrier of (InclPoset (Ids S)) ; :: thesis: f . x = g . x

then x in { X where X is Ideal of S : verum } by A8, WAYBEL_0:def 23;

then ex I being Ideal of S st x = I ;

then reconsider I = x as Ideal of S ;

A10: ex J2 being Subset of L st

( I = J2 & g . I = downarrow J2 ) by A7;

ex J1 being Subset of L st

( I = J1 & f . I = downarrow J1 ) by A6;

hence f . x = g . x by A10; :: thesis: verum

end;assume x in the carrier of (InclPoset (Ids S)) ; :: thesis: f . x = g . x

then x in { X where X is Ideal of S : verum } by A8, WAYBEL_0:def 23;

then ex I being Ideal of S st x = I ;

then reconsider I = x as Ideal of S ;

A10: ex J2 being Subset of L st

( I = J2 & g . I = downarrow J2 ) by A7;

ex J1 being Subset of L st

( I = J1 & f . I = downarrow J1 ) by A6;

hence f . x = g . x by A10; :: thesis: verum

dom f = the carrier of (InclPoset (Ids S)) by FUNCT_2:def 1;

hence f = g by A11, A9, FUNCT_1:2; :: thesis: verum