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 A1: c in dom (1 / f) ; :: thesis: (1 / f) . c = 1. / (f . c)
A2: (1 / f) . c = (R_EAL 1) / (f . c) by A1, Def9;
thus (1 / f) . c = 1. / (f . c) by A2; :: thesis: verum

end;