let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g
let f, g be PartFunc of X,Y; :: thesis: ( ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g implies f = g )
assume A1: for y being set holds Y <> {y} ; :: thesis: ( not TotFuncs f = TotFuncs g or f = g )
assume TotFuncs f = TotFuncs g ; :: thesis: f = g
then ( g c= f & f c= g ) by A1, Th167;
hence f = g by XBOOLE_0:def 10; :: thesis: verum