let f be PartFunc of REAL,REAL; :: thesis: f / f = ((dom f) \ (f " {0})) --> 1
A1: dom (f / f) = (dom f) /\ ((dom f) \ (f " {0})) by RFUNCT_1:def 1
.= (dom f) \ (f " {0}) by XBOOLE_1:28, XBOOLE_1:36 ;
for c being object st c in dom (f / f) holds
(f / f) . c = 1
proof
let c be object ; :: thesis: ( c in dom (f / f) implies (f / f) . c = 1 )
reconsider cc = c as set by TARSKI:1;
assume A2: c in dom (f / f) ; :: thesis: (f / f) . c = 1
then ( c in dom f & not c in f " {0} ) by A1, XBOOLE_0:def 5;
then not f . c in {0} by FUNCT_1:def 7;
then A3: f . c <> 0 by TARSKI:def 1;
(f / f) . c = (f . cc) * ((f . cc) ") by A2, RFUNCT_1:def 1;
hence (f / f) . c = 1 by A3, XCMPLX_0:def 7; :: thesis: verum
end;
hence f / f = ((dom f) \ (f " {0})) --> 1 by A1, FUNCOP_1:11; :: thesis: verum