let x, y, z be set ; :: thesis: for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds
y = z
let f, g be Function; :: thesis: ( f tolerates g & [x,y] in f & [x,z] in g implies y = z )
assume f tolerates g ; :: thesis: ( not [x,y] in f or not [x,z] in g or y = z )
then consider h being Function such that
A1: h = f \/ g by Th130;
assume ( [x,y] in f & [x,z] in g ) ; :: thesis: y = z
then ( [x,y] in h & [x,z] in h ) by A1, XBOOLE_0:def 3;
hence y = z by FUNCT_1:def 1; :: thesis: verum