let a, b, c, d be set ; :: thesis: ( <*a,b*> = <*c,d*> implies ( a = c & b = d ) )
assume A1: <*a,b*> = <*c,d*> ; :: thesis: ( a = c & b = d )
thus a = <*a,b*> . 1 by Th61
.= c by A1, Th61 ; :: thesis: b = d
thus b = <*a,b*> . 2 by Th61
.= d by A1, Th61 ; :: thesis: verum