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