let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds
f = g
let f, g be PartFunc of X,Y; :: thesis: ( f is total & g is total & f tolerates g implies f = g )
assume ( dom f = X & dom g = X ) ; :: according to PARTFUN1:def 2 :: thesis: ( not f tolerates g or f = g )
hence ( not f tolerates g or f = g ) by Th136; :: thesis: verum