let S, T be complete LATTICE; :: thesis: for f being idempotent Function of T,T
for h being Function of S,(Image f) holds f * h = h
let f be idempotent Function of T,T; :: thesis: for h being Function of S,(Image f) holds f * h = h
let h be Function of S,(Image f); :: thesis: f * h = h
rng h c= the carrier of (Image f) ;
then A1: rng h c= rng f by YELLOW_0:def 15;
f * f = f by QUANTAL1:def 9;
then rng f c= dom f by FUNCT_1:15;
then rng h c= dom f by A1;
hence f * h = h by A1, YELLOW16:4; :: thesis: verum