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 VectSpStr(# the carrier of V,the addF of V,the ZeroF of V,the lmult of V #) by RLVECT_1:3;
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:12;
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 7; :: thesis: verum