let f1, f2 be Function; :: thesis: ( f1 tolerates f2 implies for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2 )
assume A1: f1 tolerates f2 ; :: thesis: for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
then A2: f1 +* f2 = f1 \/ f2 by FUNCT_4:30;
let g1 be rng-retract of f1; :: thesis: for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
let g2 be rng-retract of f2; :: thesis: g1 +* g2 is rng-retract of f1 +* f2
A3: dom g1 = rng f1 by Def2;
A4: dom g2 = rng f2 by Def2;
thus dom (g1 +* g2) = (dom g1) \/ (dom g2) by FUNCT_4:def 1
.= rng (f1 +* f2) by A2, A3, A4, RELAT_1:12 ; :: according to ALGSPEC1:def 2 :: thesis: (f1 +* f2) * (g1 +* g2) = id (rng (f1 +* f2))
A5: rng g2 c= dom f2 by Th24;
rng g1 c= dom f1 by Th24;
hence (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A1, A5, FUNCT_4:69
.= (id (rng f1)) +* (f2 * g2) by Def2
.= (id (rng f1)) +* (id (rng f2)) by Def2
.= id ((rng f1) \/ (rng f2)) by FUNCT_4:22
.= id (rng (f1 +* f2)) by A2, RELAT_1:12 ;
:: thesis: verum