let C be non empty set ; :: thesis: 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) ) )
let f be PartFunc of C,ExtREAL; :: thesis: ( 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) ) )
thus dom (1 / f) = (dom f) \ (f " {0.}) by Def9; :: thesis: for c being Element of C st c in dom (1 / f) holds
(1 / f) . c = 1. / (f . c)
thus for c being Element of C st c in dom (1 / f) holds
(1 / f) . c = 1. / (f . c) :: thesis: verum

proof

let c be Element of C; :: thesis: ( c in dom (1 / f) implies (1 / f) . c = 1. / (f . c) )
assume c in dom (1 / f) ; :: thesis: (1 / f) . c = 1. / (f . c)
then (1 / f) . c = (R_EAL 1) / (f . c) by Def9;
hence (1 / f) . c = 1. / (f . c) ; :: thesis: verum

end;