for C being non empty set
for f being PartFunc of C,ExtREAL holds
( dom (1 / f) = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom (1 / f) holds
(1 / f) . c = 1. / (f . c) ) ) by Def9;