let f, g be Function; :: thesis: f +* g c= f \/ g
let p be set ; :: 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 set such that
A2: p = [x,y] by RELAT_1:def 1;
x in dom (f +* g) by A1, A2, FUNCT_1:8;
then ( ( x in dom f & not x in dom g ) or x in dom g ) by Th13;
then A3: ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th12, Th14;
y = (f +* g) . x by A1, A2, FUNCT_1:8;
then ( p in f or p in g ) by A2, A3, FUNCT_1:8;
hence p in f \/ g by XBOOLE_0:def 3; :: thesis: verum