let D, C be non empty set ; :: thesis: for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f = g
let f, g be PartFunc of C,D; :: thesis: ( dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) implies f = g )
assume A1: ( dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) ; :: thesis: f = g

now

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A2: x in dom f ; :: thesis: f . x = g . x
then reconsider y = x as Element of C ;
f /. y = g /. y by A1, A2;
then f . y = g /. y by A2, PARTFUN1:def 8;
hence f . x = g . x by A1, A2, PARTFUN1:def 8; :: thesis: verum

end;

hence f = g by A1, FUNCT_1:9; :: thesis: verum