let V be free finite-rank Z_Module; :: 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 #) ;
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 ZMODUL02:64;
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