let t1, t2 be Element of [: the carrier of V, the carrier of V:]; :: thesis: ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 implies t1 = t2 )
assume ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 ) ; :: thesis: t1 = t2
then A3: ( t1 `1 = t2 `1 & t1 `2 = t2 `2 ) by A1, Th43;
t1 = [(t1 `1),(t1 `2)] by MCART_1:21;
hence t1 = t2 by A3, MCART_1:21; :: thesis: verum