let x be object ; :: thesis: for f, g, h being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
let f, g, h be Function; :: thesis: ( h = f \/ g implies ( x in dom h iff ( x in dom f or x in dom g ) ) )
assume A1: h = f \/ g ; :: thesis: ( x in dom h iff ( x in dom f or x in dom g ) )
thus ( not x in dom h or x in dom f or x in dom g ) :: thesis: ( ( x in dom f or x in dom g ) implies x in dom h )

proof

assume x in dom h ; :: thesis: ( x in dom f or x in dom g )
then [x,(h . x)] in h by FUNCT_1:def 2;
then ( [x,(h . x)] in f or [x,(h . x)] in g ) by A1, XBOOLE_0:def 3;
hence ( x in dom f or x in dom g ) by XTUPLE_0:def 12; :: thesis: verum

end;

assume ( x in dom f or x in dom g ) ; :: thesis: x in dom h
then ( [x,(f . x)] in f or [x,(g . x)] in g ) by FUNCT_1:def 2;
then ( [x,(f . x)] in h or [x,(g . x)] in h ) by A1, XBOOLE_0:def 3;
hence x in dom h by XTUPLE_0:def 12; :: thesis: verum