set FF = <*F*>;
let x1, x2, y1, y2 be object ; :: according to FLEXARY1:def 6 :: thesis: ( x1 in dom <*F*> & y1 in dom (<*F*> . x1) & x2 in dom <*F*> & y2 in dom (<*F*> . x2) & <*F*> _ (x1,y1) = <*F*> _ (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume A1: ( x1 in dom <*F*> & y1 in dom (<*F*> . x1) & x2 in dom <*F*> & y2 in dom (<*F*> . x2) & <*F*> _ (x1,y1) = <*F*> _ (x2,y2) ) ; :: thesis: ( x1 = x2 & y1 = y2 )
( dom <*F*> = Seg 1 & Seg 1 = {1} ) by FINSEQ_1:2, FINSEQ_1:38;
then ( x1 = 1 & x2 = 1 & <*F*> . 1 = F ) by A1, TARSKI:def 1;
hence ( x1 = x2 & y1 = y2 ) by A1, FUNCT_1:def 4; :: thesis: verum