let K be non empty addLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for v being Vector of V
for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . v,(u + w) = (f . v,u) + (f . v,w)
let V, W be non empty VectSpStr of K; :: thesis: for v being Vector of V
for u, w being Vector of W
for f being Form 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 Form 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 Form of V,W st f is additiveFAF holds
f . v,(y + z) = (f . v,y) + (f . v,z)
let f be Form of V,W; :: thesis: ( f is additiveFAF implies f . v,(y + z) = (f . v,y) + (f . v,z) )
set F = FunctionalFAF f,v;
assume f is additiveFAF ; :: thesis: f . v,(y + z) = (f . v,y) + (f . v,z)
then A1: FunctionalFAF f,v is additive by Def12;
thus f . v,(y + z) = (FunctionalFAF f,v) . (y + z) by Th9
.= ((FunctionalFAF f,v) . y) + ((FunctionalFAF f,v) . z) by A1, GRCAT_1:def 13
.= (f . v,y) + ((FunctionalFAF f,v) . z) by Th9
.= (f . v,y) + (f . v,z) by Th9 ; :: thesis: verum