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