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

now

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

let x be set ; :: 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
( g . x in Y & Y <> {(g . x)} ) by A2, A4, PARTFUN1:27;
then consider y being set such that
A6: y in Y and
A7: y <> g . x by ZFMISC_1:41;
defpred S₁[ set ] means $1 in dom f;
deffunc H₁( set ) -> set = f . $1;
deffunc H₂( set ) -> set = y;
A8: for x' being set st x' in X holds
( ( S₁[x'] implies H₁(x') in Y ) & ( not S₁[x'] implies H₂(x') in Y ) ) by A6, PARTFUN1:27;
consider h being Function of X,Y such that
A9: for x' being set st x' in X holds
( ( S₁[x'] implies h . x' = H₁(x') ) & ( not S₁[x'] implies h . x' = H₂(x') ) ) from FUNCT_2:sch 5(A8);
A10: x in X by A4;
f tolerates h

proof

let x' be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x' in (dom f) /\ (dom h) or f . x' = h . x' )
assume x' in (dom f) /\ (dom h) ; :: thesis: f . x' = h . x'
then ( x' in dom f & x' in dom h ) by XBOOLE_0:def 4;
hence f . x' = h . x' by A9; :: thesis: verum

end;

then h in TotFuncs f by A3, PARTFUN1:def 7;
then ( h in TotFuncs g & x in dom h ) by A1, A3, A10, Def1;
then ( g tolerates h & x in (dom g) /\ (dom h) & h . x = y ) by A4, A5, A9, PARTFUN1:171, XBOOLE_0:def 4;
hence contradiction by A7, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

end;

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