let f, g be Element of (RAlgebra REAL); :: thesis: f - g = (@ f) - (@ g)
A1: @ ((- 1) * g) = - (@ g) by Th17;
f - g = (@ f) + (@ (- g)) by FUNCSDOM:28
.= (@ f) + (- (@ g)) by A1, RLVECT_1:16 ;
hence f - g = (@ f) - (@ g) ; :: thesis: verum