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

proof

let x be object ; :: 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 Th16;
A3: closure_op x is Element of (ClOpers L) by Th10;
(ClImageMap L) . (closure_op x) = Image (closure_op x) by Def4
.= x by Th18 ;
hence x in rng (ClImageMap L) by A2, A3, FUNCT_1:def 3; :: thesis: verum

end;

then A4: the carrier of ((ClosureSystems L) opp) = rng (ClImageMap L) ;
dom ((ClImageMap L) ") = rng (ClImageMap L) by FUNCT_1:33;
hence (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L) by A1, A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum