let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum