let f1, f2 be complex-valued Function; :: thesis: f1 - f2 = (- 1) (#) (f2 - f1)
A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12
.= dom ((- 1) (#) (f2 - f1)) by VALUED_1:def 5 ;

now :: thesis: for c being object st c in dom (f1 - f2) holds
(f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c

A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12 ;
let c be object ; :: thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c )
assume A3: c in dom (f1 - f2) ; :: thesis: (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c
thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A3, VALUED_1:13
.= (- 1) * ((f2 . c) - (f1 . c))
.= (- 1) * ((f2 - f1) . c) by A3, A2, VALUED_1:13
.= ((- 1) (#) (f2 - f1)) . c by A1, A3, VALUED_1:def 5 ; :: thesis: verum

end;

hence f1 - f2 = (- 1) (#) (f2 - f1) by A1, FUNCT_1:2; :: thesis: verum