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

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