let h, g be Function; :: thesis: ( dom h = (dom f) \ (f " {0}) & ( for c being object st c in dom h holds
h . c = (f . c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being object st c in dom g holds
g . c = (f . c) " ) implies h = g )
assume that
A1: dom h = (dom f) \ (f " {0}) and
A2: for c being object st c in dom h holds
h . c = (f . c) " and
A3: dom g = (dom f) \ (f " {0}) and
A4: for c being object st c in dom g holds
g . c = (f . c) " ; :: thesis: h = g

now :: thesis: for x being object st x in dom h holds
h . x = g . x

let x be object ; :: thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; :: thesis: h . x = g . x
hence h . x = (f . x) " by A2
.= g . x by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence h = g by A1, A3, FUNCT_1:2; :: thesis: verum