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

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