let f, g, h be Function; :: thesis: ( f c= h & g c= h implies f +* g c= h )
assume ( f c= h & g c= h ) ; :: thesis: f +* g c= h
then A1: f \/ g c= h by XBOOLE_1:8;
f +* g c= f \/ g by Th29;
hence f +* g c= h by A1; :: thesis: verum