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