let K be non empty addLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for v, u being Vector of V
for w being Vector of W
for f being Form of V,W st f is additiveSAF holds
f . (v + u),w = (f . v,w) + (f . u,w)
let V, W be non empty VectSpStr of K; :: thesis: for v, u being Vector of V
for w being Vector of W
for f being Form 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 Form 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 Form of V,W st f is additiveSAF holds
f . (v + w),y = (f . v,y) + (f . w,y)
let f be Form of V,W; :: thesis: ( f is additiveSAF implies f . (v + w),y = (f . v,y) + (f . w,y) )
set F = FunctionalSAF f,y;
assume f is additiveSAF ; :: thesis: f . (v + w),y = (f . v,y) + (f . w,y)
then A1: FunctionalSAF f,y is additive by Def13;
thus f . (v + w),y = (FunctionalSAF f,y) . (v + w) by Th10
.= ((FunctionalSAF f,y) . v) + ((FunctionalSAF f,y) . w) by A1, HAHNBAN1:def 11
.= (f . v,y) + ((FunctionalSAF f,y) . w) by Th10
.= (f . v,y) + (f . w,y) by Th10 ; :: thesis: verum