let X, Y be set ; 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; ( dom g c= dom f & TotFuncs f c= TotFuncs g implies g c= f )
assume A1:
dom g c= dom f
; ( not TotFuncs f c= TotFuncs g or g c= f )
now ( not TotFuncs f c= TotFuncs g or g c= f )per cases
not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} )
;
suppose A2:
(
Y = {} implies
X = {} )
;
( TotFuncs f c= TotFuncs g implies g c= f )thus
(
TotFuncs f c= TotFuncs g implies
g c= f )
verumproof
assume A3:
TotFuncs f c= TotFuncs g
;
g c= f
for
x being
object st
x in dom g holds
g . x = f . x
proof
let x be
object ;
( 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
;
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;
verum
end;
hence
g c= f
by A1, GRFUNC_1:2;
verum
end; end; end; end;
hence
( not TotFuncs f c= TotFuncs g or g c= f )
; verum