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 A3: Y <> {} ; :: thesis: dom g c= dom f
thus dom g c= dom f :: thesis: verum
proof
deffunc H1( object ) -> set = f . $1;
defpred S1[ 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 H2( object ) -> object = y;
A9: for x9 being object st x9 in X holds
( ( S1[x9] implies H1(x9) in Y ) & ( not S1[x9] implies H2(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
( ( S1[x9] implies h . x9 = H1(x9) ) & ( not S1[x9] implies h . x9 = H2(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