per cases ( x in dom F or not x in dom F ) ;

suppose A1: x in dom F ; :: thesis: F . x is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (F . x) or not x2 in dom (F . x) or not (F . x) . x1 = (F . x) . x2 or x1 = x2 )
assume A2: ( x1 in dom (F . x) & x2 in dom (F . x) & (F . x) . x1 = (F . x) . x2 ) ; :: thesis: x1 = x2
then F _ (x,x1) = F _ (x,x2) ;
hence x1 = x2 by A2, A1, Def6; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . x is one-to-one

hence F . x is one-to-one by FUNCT_1:def 2; :: thesis: verum

end;

end;