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;
set h = g1 union g2;
C1: dom g = A1 \/ A2 by FUNCT_2:def 1
.= dom (g1 union g2) by FUNCT_2:def 1 ;
for x being object st x in dom g holds
g . x = (g1 union g2) . x
proof
let x be object ; :: thesis: ( x in dom g implies g . x = (g1 union g2) . x )
assume x in dom g ; :: thesis: g . x = (g1 union g2) . x
then D0: ( x in A1 or x in A2 ) by XBOOLE_0:def 3;
per cases ( x in dom g2 or not x in dom g2 ) ;
suppose D1: x in dom g2 ; :: thesis: g . x = (g1 union g2) . x
then (g1 union g2) . x = g2 . x by FUNCT_4:13
.= g . x by A1, FUNCT_1:49, D1 ;
hence g . x = (g1 union g2) . x ; :: thesis: verum
end;
suppose D1: not x in dom g2 ; :: thesis: g . x = (g1 union g2) . x
then D2: x in A1 by D0, FUNCT_2:def 1;
(g1 union g2) . x = g1 . x by D1, FUNCT_4:11
.= g . x by A1, FUNCT_1:49, D2 ;
hence g . x = (g1 union g2) . x ; :: thesis: verum
end;
end;
end;
hence g = g1 union g2 by C1, FUNCT_1:2; :: thesis: verum