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 by MCART_1:48;
hence ( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 implies x = y ) by MCART_1:48; :: thesis: verum