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

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 set st x in dom g holds
g . x = f . x

proof

let x be set ; :: thesis: ( x in dom g implies g . x = f . x )
assume A4: x in dom g ; :: thesis: g . x = f . x
consider h being Function of X,Y such that
A5: f tolerates h by A2, Th148;
h in TotFuncs f by A2, A5, PARTFUN1:def 7;
then ( g tolerates h & x in dom f ) by A1, A3, A4, PARTFUN1:171;
then ( f tolerates g & x in (dom f) /\ (dom g) ) by A2, A4, A5, PARTFUN1:158, XBOOLE_0:def 4;
hence g . x = f . x by PARTFUN1:def 6; :: thesis: verum

end;

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

end;

end;

end;

end;

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