let x, y be object ; :: 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, Th7
.= (X --> a) . y by A2, Th7 ; :: thesis: verum