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: <*a1,a2*> = <*b1,b2*> by ZFMISC_1:33;
( <*a1,a2*> . 1 = a1 & <*a1,a2*> . 2 = a2 ) by FINSEQ_1:61;
hence ( a1 = b1 & a2 = b2 ) by A1, FINSEQ_1:61; :: thesis: verum