let V, W be Z_Module; for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let v be Vector of V; for w, t being Vector of W
for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let y, z be Vector of W; for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
let f be additiveFAF homogeneousFAF FrForm of V,W; f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
thus f . (v,(y - z)) =
(f . (v,y)) + (f . (v,(- z)))
by HTh27
.=
(f . (v,y)) + (f . (v,((- (1. INT.Ring)) * z)))
by VECTSP_1:14
.=
(f . (v,y)) + ((- (1. INT.Ring)) * (f . (v,z)))
by HTh32
.=
(f . (v,y)) - (f . (v,z))
; verum