let f, g be Function; :: thesis: f +* g c= f \/ g
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in f +* g or p in f \/ g )
assume A1: p in f +* g ; :: thesis: 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; :: thesis: verum