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