let A, B be non empty set ; :: thesis: for A1, A2 being non empty Subset of A
for g being Function of (A1 \/ A2),B
for g1 being Function of A1,B
for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds
g = g1 union g2
let A1, A2 be non empty Subset of A; :: thesis: for g being Function of (A1 \/ A2),B
for g1 being Function of A1,B
for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds
g = g1 union g2
let g be Function of (A1 \/ A2),B; :: thesis: for g1 being Function of A1,B
for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds
g = g1 union g2
let g1 be Function of A1,B; :: thesis: for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds
g = g1 union g2
let g2 be Function of A2,B; :: thesis: ( g | A1 = g1 & g | A2 = g2 implies g = g1 union g2 )
assume A1: ( g | A1 = g1 & g | A2 = g2 ) ; :: thesis: g = g1 union g2
A2 c= A1 \/ A2 by XBOOLE_1:7;
then reconsider f2 = g | A2 as Function of A2,B by FUNCT_2:32;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then reconsider f1 = g | A1 as Function of A1,B by FUNCT_2:32;
A2: A1 /\ A2 c= A2 by XBOOLE_1:17;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then f1 | (A1 /\ A2) = g | (A1 /\ A2) by FUNCT_1:51
.= f2 | (A1 /\ A2) by A2, FUNCT_1:51 ;
hence g = g1 union g2 by A1, Def1; :: thesis: verum