let X, Y be set ; :: thesis: for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ) holds
f1 = f2
let f1, f2 be PartFunc of X,Y; :: thesis: ( dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ) implies f1 = f2 )
assume that
A1: dom f1 = dom f2 and
A2: for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ; :: thesis: f1 = f2
for x being set st x in dom f1 holds
f1 . x = f2 . x by A2;
hence f1 = f2 by A1, FUNCT_1:9; :: thesis: verum