let A, a, b be set ; :: thesis: (A --> a) +* (A --> b) = A --> b
set g = A --> b;
dom (A --> b) = A by FUNCOP_1:19;
then dom (A --> a) c= dom (A --> b) ;
hence (A --> a) +* (A --> b) = A --> b by FUNCT_4:20; :: thesis: verum