let x, y, z be object ; :: thesis: (x .--> y) +* (x .--> z) = x .--> z
A1: dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
.= {x} ;
dom (x .--> z) = dom ({x} --> z) by FUNCOP_1:def 9
.= {x} ;
hence (x .--> y) +* (x .--> z) = x .--> z by A1, FUNCT_4:19; :: thesis: verum