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