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) & y = (f +* g) . x ) by A1, A2, FUNCT_1:8;
then ( ( x in dom f & not x in dom g ) or x in dom g ) by Th13;
then ( y = (f +* g) . x & ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) ) by A1, A2, Th12, Th14, FUNCT_1:8;
then ( p in f or p in g ) by A2, FUNCT_1:8;
hence p in f \/ g by XBOOLE_0:def 3; :: thesis: verum