let a1, b1, a2, b2, a3, b3 be set ; ( compsym (a1,a2,a3) = compsym (b1,b2,b3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) )
A1:
<*a1,a2,a3*> . 3 = a3
by FINSEQ_1:45;
assume
compsym (a1,a2,a3) = compsym (b1,b2,b3)
; ( 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 )
by FINSEQ_1:45;
hence
( a1 = b1 & a2 = b2 & a3 = b3 )
by A2, A1, FINSEQ_1:45; verum