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
consider x being Element of Carrier l;
ex a being Vector of V st
( x = a & l . a <> 0. K ) by A3, VECTSP_6:19;
hence contradiction by A1, LMOD_6:5; :: thesis: verum

end;

now

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

end;

hence Lin A is trivial by STRUCT_0:def 19; :: thesis: verum