let L be complete LATTICE; :: thesis: (ClImageMap L) " is Function of ((ClosureSystems L) opp ),(ClOpers L)
set f = ClImageMap L;
A1: ( dom ((ClImageMap L) " ) = rng (ClImageMap L) & rng ((ClImageMap L) " ) = dom (ClImageMap L) ) by FUNCT_1:55;
A2: ( dom (ClImageMap L) = the carrier of (ClOpers L) & rng (ClImageMap L) c= the carrier of ((ClosureSystems L) opp ) ) by FUNCT_2:def 1;
the carrier of ((ClosureSystems L) opp ) c= rng (ClImageMap L)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((ClosureSystems L) opp ) or x in rng (ClImageMap L) )
assume x in the carrier of ((ClosureSystems L) opp ) ; :: thesis: x in rng (ClImageMap L)
then reconsider x = x as Element of ((ClosureSystems L) opp ) ;
reconsider x = x as strict full infs-inheriting SubRelStr of L by Th17;
A3: closure_op x is Element of (ClOpers L) by Th11;
(ClImageMap L) . (closure_op x) = Image (closure_op x) by Def5
.= x by Th19 ;
hence x in rng (ClImageMap L) by A2, A3, FUNCT_1:def 5; :: thesis: verum

end;

then the carrier of ((ClosureSystems L) opp ) = rng (ClImageMap L) by XBOOLE_0:def 10;
hence (ClImageMap L) " is Function of ((ClosureSystems L) opp ),(ClOpers L) by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum