let f1, f2 be Function; :: thesis: ( f1 c= f2 implies for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2 )
assume A1: f1 c= f2 ; :: thesis: for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2
A2: f2 +* f1 = f2 by A1, FUNCT_4:98;
set g = the rng-retract of f2;
let g1 be rng-retract of f1; :: thesis: ex g2 being rng-retract of f2 st g1 c= g2
f1 tolerates f2 by A1, PARTFUN1:52;
then reconsider g2 = the rng-retract of f2 +* g1 as rng-retract of f2 by A2, Th27;
take g2 ; :: thesis: g1 c= g2
thus g1 c= g2 by FUNCT_4:25; :: thesis: verum