let K be non empty addLoopStr ; :: thesis: for V, W being non empty ModuleStr over 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 ModuleStr over 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 ;

thus f . ((v + w),y) = (FunctionalSAF (f,y)) . (v + w) by Th9

.= ((FunctionalSAF (f,y)) . v) + ((FunctionalSAF (f,y)) . w) by A1

.= (f . (v,y)) + ((FunctionalSAF (f,y)) . w) by Th9

.= (f . (v,y)) + (f . (w,y)) by Th9 ; :: thesis: verum

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 ModuleStr over 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 ;

thus f . ((v + w),y) = (FunctionalSAF (f,y)) . (v + w) by Th9

.= ((FunctionalSAF (f,y)) . v) + ((FunctionalSAF (f,y)) . w) by A1

.= (f . (v,y)) + ((FunctionalSAF (f,y)) . w) by Th9

.= (f . (v,y)) + (f . (w,y)) by Th9 ; :: thesis: verum