let A be non empty set ; :: thesis: for f being Element of (RAlgebra A) holds
( (- 1) * f = (- 1) (#) (@ f) & @ ((- 1) * f) = - (@ f) & 0. (RAlgebra A) = 0 (#) (@ f) )
let f be Element of (RAlgebra A); :: thesis: ( (- 1) * f = (- 1) (#) (@ f) & @ ((- 1) * f) = - (@ f) & 0. (RAlgebra A) = 0 (#) (@ f) )
0. (RAlgebra A) = A --> 0
.= 0 (#) (@ f) ;
hence ( (- 1) * f = (- 1) (#) (@ f) & @ ((- 1) * f) = - (@ f) & 0. (RAlgebra A) = 0 (#) (@ f) ) by FUNCSDOM:30; :: thesis: verum