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
set P = InclPoset (Ids S);
A8: ( dom f = the carrier of (InclPoset (Ids S)) & dom g = the carrier of (InclPoset (Ids S)) ) by FUNCT_2:def 1;
A9: the carrier of (InclPoset (Ids S)) = the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def 1
.= Ids S ;

now

let x be set ; :: 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 A9, WAYBEL_0:def 23;
then ex I being Ideal of S st x = I ;
then reconsider I = x as Ideal of S ;
consider J1 being Subset of L such that
A10: I = J1 and
A11: f . I = downarrow J1 by A6;
consider J2 being Subset of L such that
A12: I = J2 and
A13: g . I = downarrow J2 by A7;
thus f . x = g . x by A10, A11, A12, A13; :: thesis: verum

end;

hence f = g by A8, FUNCT_1:9; :: thesis: verum