let K be Field; :: thesis: for V3, V2 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 V3, V2 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, Th20
.= Sum (lmlt a,(g * b2)) by A1, A2, Th21 ; :: thesis: verum