let a, b, c, d, e, f be object ; :: 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
.= d by A1, Th45 ; :: thesis: ( b = e & c = f )
thus b = <*a,b,c*> . 2
.= e by A1, Th45 ; :: thesis: c = f
thus c = <*a,b,c*> . 3
.= f by A1, Th45 ; :: thesis: verum