let x, y be set ; :: according to FUNCT_1:def 10 :: thesis: ( not x in proj1 (X --> a) or not y in proj1 (X --> a) or (X --> a) . x = (X --> a) . y )
assume that
A1: x in dom (X --> a) and
A2: y in dom (X --> a) ; :: thesis: (X --> a) . x = (X --> a) . y
thus (X --> a) . x = a by A1, Th13
.= (X --> a) . y by A2, Th13 ; :: thesis: verum