let T be non empty TopSpace; :: thesis: for f being Function of T,T st f * f = f holds
(corestr f) * (incl (Image f)) = id (Image f)
let f be Function of T,T; :: thesis: ( f * f = f implies (corestr f) * (incl (Image f)) = id (Image f) )
assume A1: f * f = f ; :: thesis: (corestr f) * (incl (Image f)) = id (Image f)
set cf = corestr f;
set i = incl (Image f);
for x being object st x in the carrier of (Image f) holds
((corestr f) * (incl (Image f))) . x = (id (Image f)) . x
proof
A2: the carrier of (Image f) c= the carrier of T by BORSUK_1:1;
let x be object ; :: thesis: ( x in the carrier of (Image f) implies ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x )
assume A3: x in the carrier of (Image f) ; :: thesis: ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x
the carrier of (Image f) = rng f by WAYBEL18:9;
then A4: ex y being object st
( y in dom f & f . y = x ) by A3, FUNCT_1:def 3;
thus ((corestr f) * (incl (Image f))) . x = (corestr f) . ((incl (Image f)) . x) by A3, FUNCT_2:15
.= (corestr f) . x by A3, A2, TMAP_1:84
.= f . x by WAYBEL18:def 7
.= x by A1, A4, FUNCT_2:15
.= (id (Image f)) . x by A3, FUNCT_1:18 ; :: thesis: verum
end;
hence (corestr f) * (incl (Image f)) = id (Image f) ; :: thesis: verum