let R be Ring; for V being RightMod of R
for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let V be RightMod of R; for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let v1, v2 be Vector of V; for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let L be Linear_Combination of V; ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) )
assume that
A1:
Carrier L = {v1,v2}
and
A2:
v1 <> v2
; Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
L is Linear_Combination of {v1,v2}
by A1, Def5;
hence
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
by A2, Th33; verum