let f be Function; :: thesis: for g being rng-retract of f
for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )
let g be rng-retract of f; :: thesis: for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )
let x be set ; :: thesis: ( x in rng f implies ( g . x in dom f & f . (g . x) = x ) )
assume A1: x in rng f ; :: thesis: ( g . x in dom f & f . (g . x) = x )
A2: dom g = rng f by Def2;
then ( g . x in rng g & rng g c= dom f ) by A1, Th24, FUNCT_1:def 5;
hence g . x in dom f ; :: thesis: f . (g . x) = x
thus f . (g . x) = (f * g) . x by A1, A2, FUNCT_1:23
.= (id (rng f)) . x by Def2
.= x by A1, FUNCT_1:35 ; :: thesis: verum