let x, y be set ; :: according to FUNCT_1:def 16 :: thesis: ( not x in dom (X --> a) or not y in dom (X --> a) or (X --> a) . x = (X --> a) . y )
A1: dom (X --> a) = X by Th19;
assume A2: ( x in dom (X --> a) & y in dom (X --> a) ) ; :: thesis: (X --> a) . x = (X --> a) . y
hence (X --> a) . x = a by A1, Th13
.= (X --> a) . y by A1, A2, Th13 ;
:: thesis: verum