let V2, V3 be free finite-rank Z_Module; for g being Function of V2,V3
for b2 being OrdBasis of V2
for a being FinSequence of INT.Ring 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; for b2 being OrdBasis of V2
for a being FinSequence of INT.Ring 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; for a being FinSequence of INT.Ring 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 INT.Ring; ( 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 )
; 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
; verum