let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (x .--> y) or not x2 in proj1 (x .--> y) or not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 )
set f = x .--> y;
assume that
A1: x1 in dom (x .--> y) and
A2: x2 in dom (x .--> y) ; :: thesis: ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 )
x1 = x by A1, TARSKI:def 1;
hence ( not (x .--> y) . x1 = (x .--> y) . x2 or x1 = x2 ) by A2, TARSKI:def 1; :: thesis: verum