let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds
g c= f
let f, g be PartFunc of X,Y; :: thesis: ( dom g c= dom f & TotFuncs f c= TotFuncs g implies g c= f )
assume A1: dom g c= dom f ; :: thesis: ( not TotFuncs f c= TotFuncs g or g c= f )

now :: thesis: ( not TotFuncs f c= TotFuncs g or g c= f )

per cases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ;

suppose ( Y = {} & X <> {} ) ; :: thesis: ( not TotFuncs f c= TotFuncs g or g c= f )

hence ( not TotFuncs f c= TotFuncs g or g c= f ) ; :: thesis: verum

end;

suppose A2: ( Y = {} implies X = {} ) ; :: thesis: ( TotFuncs f c= TotFuncs g implies g c= f )

thus ( TotFuncs f c= TotFuncs g implies g c= f ) :: thesis: verum

proof

assume A3: TotFuncs f c= TotFuncs g ; :: thesis: g c= f
for x being object st x in dom g holds
g . x = f . x

proof

let x be object ; :: thesis: ( x in dom g implies g . x = f . x )
consider h being Function of X,Y such that
A4: f tolerates h by A2, Th76;
h in TotFuncs f by A2, A4, PARTFUN1:def 5;
then A5: g tolerates h by A3, PARTFUN1:71;
assume x in dom g ; :: thesis: g . x = f . x
then x in (dom f) /\ (dom g) by A1, XBOOLE_0:def 4;
hence g . x = f . x by A5, A2, A4, PARTFUN1:67, PARTFUN1:def 4; :: thesis: verum

end;

hence g c= f by A1, GRFUNC_1:2; :: thesis: verum

end;

end;

end;

end;

hence ( not TotFuncs f c= TotFuncs g or g c= f ) ; :: thesis: verum