let a, b be pair set ; :: thesis: ( a `1 = b `1 & a `2 = b `2 implies a = b )
assume Z: ( a `1 = b `1 & a `2 = b `2 ) ; :: thesis: a = b
( a = [(a `1),(a `2)] & b = [(b `1),(b `2)] ) ;
hence a = b by Z; :: thesis: verum