let L be lower-bounded sup-Semilattice; :: thesis: (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
set LS = (Rel2Map L) * (Map2Rel L);
set R = id the carrier of (MonSet L);
A1: dom ((Rel2Map L) * (Map2Rel L)) = the carrier of (MonSet L) by FUNCT_2:def 1;
A2: dom (id the carrier of (MonSet L)) = the carrier of (MonSet L) by FUNCT_1:34;
for a being set st a in the carrier of (MonSet L) holds
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a

proof

let a be set ; :: thesis: ( a in the carrier of (MonSet L) implies ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a )
assume A3: a in the carrier of (MonSet L) ; :: thesis: ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
then consider s being Function of L,(InclPoset (Ids L)) such that
A4: a = s and
s is monotone and
for x being Element of L holds s . x c= downarrow x by Def14;
((Rel2Map L) * (Map2Rel L)) . s in the carrier of (MonSet L) by A3, A4, FUNCT_2:7;
then consider Ls being Function of L,(InclPoset (Ids L)) such that
A5: ((Rel2Map L) * (Map2Rel L)) . s = Ls and
Ls is monotone and
for x being Element of L holds Ls . x c= downarrow x by Def14;
set AR = (Map2Rel L) . s;
(Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A3, A4, FUNCT_2:7;
then (Map2Rel L) . s in Aux L by YELLOW_1:1;
then reconsider AR = (Map2Rel L) . s as auxiliary Relation of L by Def9;
dom (Map2Rel L) = the carrier of (MonSet L) by FUNCT_2:def 1;
then Ls = (Rel2Map L) . AR by A3, A4, A5, FUNCT_1:23;
then A6: Ls = AR -below by Def15;
A7: dom Ls = the carrier of L by FUNCT_2:def 1;
A8: dom s = the carrier of L by FUNCT_2:def 1;

now

let b be set ; :: thesis: ( b in the carrier of L implies Ls . b = s . b )
assume A9: b in the carrier of L ; :: thesis: Ls . b = s . b
then reconsider b' = b as Element of L ;
A10: Ls . b c= s . b

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in Ls . b or d in s . b )
assume d in Ls . b ; :: thesis: d in s . b
then d in AR -below b' by A6, Def13;
then A11: [d,b'] in AR by Th13;
ex AR' being auxiliary Relation of L st
( AR' = (Map2Rel L) . s & ( for d, b' being set holds
( [d,b'] in AR' iff ex d', b'' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( d' = d & b'' = b' & s' = s & d' in s' . b'' ) ) ) ) by A3, A4, Def16;
then ex d', b'' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( d' = d & b'' = b' & s' = s & d' in s' . b'' ) by A11;
hence d in s . b ; :: thesis: verum

end;

s . b c= Ls . b

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in s . b or d in Ls . b )
assume A12: d in s . b ; :: thesis: d in Ls . b
s . b in the carrier of (InclPoset (Ids L)) by A9, FUNCT_2:7;
then s . b in Ids L by YELLOW_1:1;
then ex X being Ideal of L st s . b = X ;
then reconsider d' = d as Element of L by A12;
ex AR' being auxiliary Relation of L st
( AR' = (Map2Rel L) . s & ( for d, b' being set holds
( [d,b'] in AR' iff ex d', b'' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( d' = d & b'' = b' & s' = s & d' in s' . b'' ) ) ) ) by A3, A4, Def16;
then [d',b'] in AR by A12;
then d' in AR -below b' ;
hence d in Ls . b by A6, Def13; :: thesis: verum

end;

hence Ls . b = s . b by A10, XBOOLE_0:def 10; :: thesis: verum

end;

then Ls = s by A7, A8, FUNCT_1:9;
hence ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a by A3, A4, A5, FUNCT_1:35; :: thesis: verum

end;

hence (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) by A1, A2, FUNCT_1:9; :: thesis: verum