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