let a, b be quadruple object ; :: thesis: ( a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 implies a = b )
assume A1: ( a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 ) ; :: thesis: a = b
( a = [(a `1_4),(a `2_4),(a `3_4),(a `4_4)] & b = [(b `1_4),(b `2_4),(b `3_4),(b `4_4)] ) ;
hence a = b by A1; :: thesis: verum