let L be non empty Poset; :: thesis: for f being Function of L,L st f is idempotent holds
(corestr f) * (inclusion f) = id (Image f)
let f be Function of L,L; :: thesis: ( f is idempotent implies (corestr f) * (inclusion f) = id (Image f) )
assume A1: f is idempotent ; :: thesis: (corestr f) * (inclusion f) = id (Image f)
for s being Element of (Image f) holds ((corestr f) * (inclusion f)) . s = s
proof
let s be Element of (Image f); :: thesis: ((corestr f) * (inclusion f)) . s = s
the carrier of (Image f) = rng (corestr f) by FUNCT_2:def 3;
then consider l being object such that
A2: l in the carrier of L and
A3: (corestr f) . l = s by FUNCT_2:11;
reconsider l = l as Element of L by A2;
A4: (corestr f) . l = f . l by Th30;
thus ((corestr f) * (inclusion f)) . s = (corestr f) . ((inclusion f) . s) by FUNCT_2:15
.= (corestr f) . s
.= f . (f . l) by A3, A4, Th30
.= s by A1, A3, A4, YELLOW_2:18 ; :: thesis: verum
end;
hence (corestr f) * (inclusion f) = id (Image f) by FUNCT_2:124; :: thesis: verum