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