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)

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

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

then A4:
the carrier of ((ClosureSystems L) opp) = rng (ClImageMap L)
;
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;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

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