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:79;
consider g being 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:131;
then reconsider g2 = g +* g1 as rng-retract of f2 by A2, Th28;
take g2 ; :: thesis: g1 c= g2
thus g1 c= g2 by FUNCT_4:26; :: thesis: verum