let a1, b1, a2, b2 be set ; :: thesis: ( homsym a1,a2 = homsym b1,b2 implies ( a1 = b1 & a2 = b2 ) )
assume homsym a1,a2 = homsym b1,b2 ; :: thesis: ( a1 = b1 & a2 = b2 )
then ( <*a1,a2*> = <*b1,b2*> & <*a1,a2*> . 1 = a1 & <*a1,a2*> . 2 = a2 ) by FINSEQ_1:61, ZFMISC_1:33;
hence ( a1 = b1 & a2 = b2 ) by FINSEQ_1:61; :: thesis: verum