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