theorem :: PRALG_1:13

for f, g being 1-sorted-yielding Function holds Carrier (f +* g) = (Carrier f) +* (Carrier g)