let a, b, c, d be object ; :: 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 Th44
.= c by A1, Th44 ; :: thesis: b = d
thus b = <*a,b*> . 2 by Th44
.= d by A1, Th44 ; :: thesis: verum