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