let x, y, z be object ; :: thesis: (x .--> y) +* (x,z) = x .--> z
dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
.= {x} ;
then x in dom (x .--> y) by TARSKI:def 1;
then (x .--> y) +* (x,z) = (x .--> y) +* (x .--> z) by FUNCT_7:def 3;
hence (x .--> y) +* (x,z) = x .--> z by Th12; :: thesis: verum