set f = x .--> y;
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (x .--> y) or not x2 in dom (x .--> y) or not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 )
A1: dom (x .--> y) = {x} by Th19;
assume ( x1 in dom (x .--> y) & x2 in dom (x .--> y) ) ; :: thesis: ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 )
then ( x1 = x & x2 = x ) by A1, TARSKI:def 1;
hence ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 ) ; :: thesis: verum