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

thus f . (v,(y + z)) = (FunctionalFAF (f,v)) . (y + z) by Th8

.= ((FunctionalFAF (f,v)) . y) + ((FunctionalFAF (f,v)) . z) by A1

.= (f . (v,y)) + ((FunctionalFAF (f,v)) . z) by Th8

.= (f . (v,y)) + (f . (v,z)) by Th8 ; :: thesis: verum

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

thus f . (v,(y + z)) = (FunctionalFAF (f,v)) . (y + z) by Th8

.= ((FunctionalFAF (f,v)) . y) + ((FunctionalFAF (f,v)) . z) by A1

.= (f . (v,y)) + ((FunctionalFAF (f,v)) . z) by Th8

.= (f . (v,y)) + (f . (v,z)) by Th8 ; :: thesis: verum