let f, g be Function; f +* g c= f \/ g
let p be object ; TARSKI:def 3 ( not p in f +* g or p in f \/ g )
assume A1:
p in f +* g
; p in f \/ g
then consider x, y being object such that
A2:
p = [x,y]
by RELAT_1:def 1;
x in dom (f +* g)
by A1, A2, FUNCT_1:1;
then
( ( x in dom f & not x in dom g ) or x in dom g )
by Th12;
then A3:
( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) )
by Th11, Th13;
y = (f +* g) . x
by A1, A2, FUNCT_1:1;
then
( p in f or p in g )
by A2, A3, FUNCT_1:1;
hence
p in f \/ g
by XBOOLE_0:def 3; verum