set FF = <*F*>;
let x1, x2, y1, y2 be object ; FLEXARY1:def 6 ( 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) )
; ( 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, FINSEQ_1:40;
hence
( x1 = x2 & y1 = y2 )
by A1, FUNCT_1:def 4; verum