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 )
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 Th13
.= (X --> a) . y by A2, Th13 ;
:: thesis: verum