let f1, f2 be PartFunc of REAL,REAL; :: thesis: (- f1) (#) (- f2) = f1 (#) f2
( dom (- f1) = dom f1 & dom (- f2) = dom f2 ) by VALUED_1:def 5;
then A1: dom ((- f1) (#) (- f2)) = (dom f1) /\ (dom f2) by VALUED_1:def 4
.= dom (f1 (#) f2) by VALUED_1:def 4 ;
for x being Element of REAL st x in dom (f1 (#) f2) holds
((- f1) (#) (- f2)) . x = (f1 (#) f2) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (f1 (#) f2) implies ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x )
assume A2: x in dom (f1 (#) f2) ; :: thesis: ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x
dom (f1 (#) f2) = (dom f2) /\ (dom f1) by VALUED_1:def 4;
then dom (f2 (#) f1) c= dom f2 by XBOOLE_1:17;
then x in dom f2 by A2;
then A3: x in dom ((- 1) (#) f2) by VALUED_1:def 5;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then dom (f1 (#) f2) c= dom f1 by VALUED_1:def 4;
then x in dom f1 by A2;
then A4: x in dom ((- 1) (#) f1) by VALUED_1:def 5;
((- f1) (#) (- f2)) . x = ((- f1) . x) * ((- f2) . x) by A1, A2, VALUED_1:def 4
.= ((- 1) * (f1 . x)) * (((- 1) (#) f2) . x) by A4, VALUED_1:def 5
.= ((- 1) * (f1 . x)) * ((- 1) * (f2 . x)) by A3, VALUED_1:def 5
.= (f1 . x) * (f2 . x) ;
hence ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x by A2, VALUED_1:def 4; :: thesis: verum

end;

hence (- f1) (#) (- f2) = f1 (#) f2 by A1, PARTFUN1:5; :: thesis: verum