let f, g be Function; :: thesis: for x being object holds
( x in dom (f +* g) iff ( x in dom f or x in dom g ) )
let x be object ; :: thesis: ( x in dom (f +* g) iff ( x in dom f or x in dom g ) )
( x in dom (f +* g) iff x in (dom f) \/ (dom g) ) by Def1;
hence ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) by XBOOLE_0:def 3; :: thesis: verum