let K be Field; :: thesis: for V2, V3 being finite-dimensional VectSp of K

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let V2, V3 be finite-dimensional VectSp of K; :: thesis: for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let g be Function of V2,V3; :: thesis: for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let b2 be OrdBasis of V2; :: thesis: for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let a be FinSequence of K; :: thesis: ( len a = len b2 & g is additive & g is homogeneous implies g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) )

assume that

A1: len a = len b2 and

A2: ( g is additive & g is homogeneous ) ; :: thesis: g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

thus g . (Sum (lmlt (a,b2))) = Sum (g * (lmlt (a,b2))) by A2, Th16

.= Sum (lmlt (a,(g * b2))) by A1, A2, Th17 ; :: thesis: verum

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let V2, V3 be finite-dimensional VectSp of K; :: thesis: for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let g be Function of V2,V3; :: thesis: for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let b2 be OrdBasis of V2; :: thesis: for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

let a be FinSequence of K; :: thesis: ( len a = len b2 & g is additive & g is homogeneous implies g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) )

assume that

A1: len a = len b2 and

A2: ( g is additive & g is homogeneous ) ; :: thesis: g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

thus g . (Sum (lmlt (a,b2))) = Sum (g * (lmlt (a,b2))) by A2, Th16

.= Sum (lmlt (a,(g * b2))) by A1, A2, Th17 ; :: thesis: verum