for f1, f2 being Function st f1 tolerates f2 holds
for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2