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