theorem :: ALGSPEC1:28

for f1, f2 being Function st f1 c= f2 holds
for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2