let X1, X2, X3 be non empty set ; :: thesis: for x, y being Element of [:X1,X2,X3:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 holds
x = y
let x, y be Element of [:X1,X2,X3:]; :: thesis: ( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 implies x = y )
( [(x `1 ),(x `2 ),(x `3 )] = x & [(y `1 ),(y `2 ),(y `3 )] = y ) by MCART_1:48;
hence ( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 implies x = y ) ; :: thesis: verum