let a, b be pair object ; :: thesis: ( a `1 = b `1 & a `2 = b `2 implies a = b )
assume A1: ( 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 A1; :: thesis: verum