let K be Ring; :: thesis: for V being LeftMod of K
for A being Subset of V st K is trivial holds
( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )
let V be LeftMod of K; :: thesis: for A being Subset of V st K is trivial holds
( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )
let A be Subset of V; :: thesis: ( K is trivial implies ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial ) )
assume A1: K is trivial ; :: thesis: ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )
thus A2: for l being Linear_Combination of A holds Carrier l = {} :: thesis: Lin A is trivial

proof

let l be Linear_Combination of A; :: thesis: Carrier l = {}
assume A3: Carrier l <> {} ; :: thesis: contradiction
set x = the Element of Carrier l;
ex a being Vector of V st
( the Element of Carrier l = a & l . a <> 0. K ) by A3, VECTSP_6:1;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: for a being Vector of (Lin A) holds a = 0. (Lin A)

let a be Vector of (Lin A); :: thesis: a = 0. (Lin A)
a in Lin A ;
then consider l being Linear_Combination of A such that
A4: a = Sum l by MOD_3:4;
Carrier l = {} by A2;
then a = 0. V by A4, VECTSP_6:19;
hence a = 0. (Lin A) by VECTSP_4:11; :: thesis: verum

end;

hence Lin A is trivial ; :: thesis: verum