let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being object holds Y <> {y} ) holds
g c= f
let f, g be PartFunc of X,Y; :: thesis: ( TotFuncs f c= TotFuncs g & ( for y being object holds Y <> {y} ) implies g c= f )
assume that
A1: TotFuncs f c= TotFuncs g and
A2: for y being object holds Y <> {y} ; :: thesis: g c= f

now :: thesis: dom g c= dom f

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: dom g c= dom f

hence dom g c= dom f ; :: thesis: verum

end;

suppose A3: Y <> {} ; :: thesis: dom g c= dom f

thus dom g c= dom f :: thesis: verum

proof

deffunc H₁( object ) -> set = f . $1;
defpred S₁[ object ] means $1 in dom f;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in dom f )
assume that
A4: x in dom g and
A5: not x in dom f ; :: thesis: contradiction
A6: Y <> {(g . x)} by A2;
g . x in Y by A4, PARTFUN1:4;
then consider y being object such that
A7: y in Y and
A8: y <> g . x by A6, ZFMISC_1:35;
deffunc H₂( object ) -> object = y;
A9: for x9 being object st x9 in X holds
( ( S₁[x9] implies H₁(x9) in Y ) & ( not S₁[x9] implies H₂(x9) in Y ) ) by A7, PARTFUN1:4;
consider h being Function of X,Y such that
A10: for x9 being object st x9 in X holds
( ( S₁[x9] implies h . x9 = H₁(x9) ) & ( not S₁[x9] implies h . x9 = H₂(x9) ) ) from FUNCT_2:sch 5(A9);
f tolerates h

proof

let x9 be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x9 in (proj1 f) /\ (proj1 h) or f . x9 = h . x9 )
assume x9 in (dom f) /\ (dom h) ; :: thesis: f . x9 = h . x9
then x9 in dom f by XBOOLE_0:def 4;
hence f . x9 = h . x9 by A10; :: thesis: verum

end;

then A11: h in TotFuncs f by A3, PARTFUN1:def 5;
x in X by A4;
then x in dom h by A3, Def1;
then A12: x in (dom g) /\ (dom h) by A4, XBOOLE_0:def 4;
h . x = y by A4, A5, A10;
hence contradiction by A8, A11, A12, A1, PARTFUN1:71, PARTFUN1:def 4; :: thesis: verum

end;

end;

end;

end;

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