let A be set ; :: thesis: for C being non empty set
for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
let C be non empty set ; :: thesis: for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
let f, g be Function of A,C; :: thesis: for B being set holds f +* (g | B) is Function of A,C
let B be set ; :: thesis: f +* (g | B) is Function of A,C
A1: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
dom (f +* (g | B)) = (dom f) \/ (dom (g | B)) by FUNCT_4:def 1
.= (dom f) \/ ((dom g) /\ B) by RELAT_1:61
.= A by A1, XBOOLE_1:22 ;
hence f +* (g | B) is Function of A,C by FUNCT_2:67; :: thesis: verum