let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for v being Vector of V
for u, w being Vector of W
for f being FrForm of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
let v be Vector of V; :: thesis: for u, w being Vector of W
for f being FrForm of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
let y, z be Vector of W; :: thesis: for f being FrForm of V,W st f is additiveFAF holds
f . (v,(y + z)) = (f . (v,y)) + (f . (v,z))
let f be FrForm of V,W; :: thesis: ( f is additiveFAF implies f . (v,(y + z)) = (f . (v,y)) + (f . (v,z)) )
set F = FrFunctionalFAF (f,v);
assume f is additiveFAF ; :: thesis: f . (v,(y + z)) = (f . (v,y)) + (f . (v,z))
then A1: FrFunctionalFAF (f,v) is additive ;
thus f . (v,(y + z)) = (FrFunctionalFAF (f,v)) . (y + z) by HTh8
.= ((FrFunctionalFAF (f,v)) . y) + ((FrFunctionalFAF (f,v)) . z) by A1
.= (f . (v,y)) + ((FrFunctionalFAF (f,v)) . z) by HTh8
.= (f . (v,y)) + (f . (v,z)) by HTh8 ; :: thesis: verum