let a, b, c, d, a9, b9, c9, d9 be object ; :: thesis: ( <*a,b,c,d*> = <*a9,b9,c9,d9*> implies ( a = a9 & b = b9 & c = c9 & d = d9 ) )
assume A1: <*a,b,c,d*> = <*a9,b9,c9,d9*> ; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 )
set x = <*a,b,c,d*>;
set y = <*a9,b9,c9,d9*>;
( <*a,b,c,d*> . 1 = a & <*a,b,c,d*> . 2 = b & <*a,b,c,d*> . 3 = c & <*a,b,c,d*> . 4 = d & <*a9,b9,c9,d9*> . 1 = a9 & <*a9,b9,c9,d9*> . 2 = b9 & <*a9,b9,c9,d9*> . 3 = c9 & <*a9,b9,c9,d9*> . 4 = d9 ) ;
hence ( a = a9 & b = b9 & c = c9 & d = d9 ) by A1; :: thesis: verum