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, Th51;
t1 = [(t1 `1 ),(t1 `2 )] by MCART_1:23;
hence t1 = t2 by A3, MCART_1:23; :: thesis: verum