let f, g be 1-sorted-yielding Function; :: thesis: ( f tolerates g implies Carrier f tolerates Carrier g )
assume A1: f tolerates g ; :: thesis: Carrier f tolerates Carrier g

now :: thesis: for x being object st x in (dom (Carrier f)) /\ (dom (Carrier g)) holds
(Carrier f) . x = (Carrier g) . x

let x be object ; :: thesis: ( x in (dom (Carrier f)) /\ (dom (Carrier g)) implies (Carrier f) . x = (Carrier g) . x )
assume x in (dom (Carrier f)) /\ (dom (Carrier g)) ; :: thesis: (Carrier f) . x = (Carrier g) . x
then x in (dom (Carrier f)) /\ (dom g) by Def13;
then A2: ( x in (dom f) /\ (dom g) & x is set ) by Def13;
then A3: ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
A4: f . x = g . x by A1, A2, PARTFUN1:def 4;
consider R1 being 1-sorted such that
A5: ( R1 = f . x & (Carrier f) . x = the carrier of R1 ) by A3, Def13;
consider R2 being 1-sorted such that
A6: ( R2 = g . x & (Carrier g) . x = the carrier of R2 ) by A3, Def13;
thus (Carrier f) . x = (Carrier g) . x by A4, A5, A6; :: thesis: verum

end;

hence Carrier f tolerates Carrier g by PARTFUN1:def 4; :: thesis: verum