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 ) )
assume compsym a1,a2,a3 = compsym b1,b2,b3 ; :: thesis: ( a1 = b1 & a2 = b2 & a3 = b3 )
then ( <*a1,a2,a3*> = <*b1,b2,b3*> & <*a1,a2,a3*> . 1 = a1 & <*a1,a2,a3*> . 2 = a2 & <*a1,a2,a3*> . 3 = a3 ) by FINSEQ_1:62, ZFMISC_1:33;
hence ( a1 = b1 & a2 = b2 & a3 = b3 ) by FINSEQ_1:62; :: thesis: verum