let a1, b1, a2, b2, a3, b3 be set ; :: thesis: ( compsym (a1,a2,a3) = compsym (b1,b2,b3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) )
A1: <*a1,a2,a3*> . 3 = a3 ;
assume compsym (a1,a2,a3) = compsym (b1,b2,b3) ; :: thesis: ( a1 = b1 & a2 = b2 & a3 = b3 )
then A2: <*a1,a2,a3*> = <*b1,b2,b3*> by XTUPLE_0:1;
( <*a1,a2,a3*> . 1 = a1 & <*a1,a2,a3*> . 2 = a2 ) ;
hence ( a1 = b1 & a2 = b2 & a3 = b3 ) by A2, A1, FINSEQ_1:45; :: thesis: verum