W1 + W2 = VectSpStr(# the carrier of M,the U7 of M,the U2 of M,the lmult of M #) by A1, Def4;
then consider v1, v2 being Element of M such that
A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm16;
take [v1,v2] ; :: thesis: ( v = ([v1,v2] `1 ) + ([v1,v2] `2 ) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
( [v1,v2] `1 = v1 & [v1,v2] `2 = v2 ) by MCART_1:7;
hence ( v = ([v1,v2] `1 ) + ([v1,v2] `2 ) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) by A2; :: thesis: verum