let K be Field; :: thesis: for V being VectSp of K

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let V be VectSp of K; :: thesis: for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let W be Element of V; :: thesis: for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let b2 be Basis of V; :: thesis: ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

W in ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by RLVECT_1:1;

then W in Lin b2 by VECTSP_7:def 3;

then consider KL1 being Linear_Combination of b2 such that

A1: W = Sum KL1 by VECTSP_7:7;

take KL = KL1; :: thesis: ( W = Sum KL & Carrier KL c= b2 )

thus W = Sum KL by A1; :: thesis: Carrier KL c= b2

thus Carrier KL c= b2 by VECTSP_6:def 4; :: thesis: verum

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let V be VectSp of K; :: thesis: for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let W be Element of V; :: thesis: for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

let b2 be Basis of V; :: thesis: ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

W in ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by RLVECT_1:1;

then W in Lin b2 by VECTSP_7:def 3;

then consider KL1 being Linear_Combination of b2 such that

A1: W = Sum KL1 by VECTSP_7:7;

take KL = KL1; :: thesis: ( W = Sum KL & Carrier KL c= b2 )

thus W = Sum KL by A1; :: thesis: Carrier KL c= b2

thus Carrier KL c= b2 by VECTSP_6:def 4; :: thesis: verum