theorem :: PRALG_1:12

for f, g being 1-sorted-yielding Function st f tolerates g holds
Carrier f tolerates Carrier g