W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 Lm13;

take [v1,v2] ; :: thesis: ( 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; :: thesis: verum

then consider v1, v2 being VECTOR of V such that

A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm13;

take [v1,v2] ; :: thesis: ( 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; :: thesis: verum