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