W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #)
by A1;
then consider v1, v2 being Vector of V such that
A2:
( v1 in W1 & v2 in W2 & v = v1 + v2 )
by Lm14;
take
[v1,v2]
; ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
thus
( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
by A2; verum