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