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: rng g c= dom f by Th24;
A3: dom g = rng f by Def2;
then g . x in rng g by A1, FUNCT_1:def 3;
hence g . x in dom f by A2; :: thesis: f . (g . x) = x
thus f . (g . x) = (f * g) . x by A1, A3, FUNCT_1:13
.= (id (rng f)) . x by Def2
.= x by A1, FUNCT_1:18 ; :: thesis: verum