let a be Element of A; :: thesis: ( a = F /. x iff a = F . x )
x in dom F by A1, Def1;
hence ( a = F /. x iff a = F . x ) by PARTFUN1:def 6; :: thesis: verum