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