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

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

hence
g = g1 union g2
by C1, FUNCT_1:2; :: thesis: verum
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;

end;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 )
;

end;

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;.= g . x by A1, FUNCT_1:49, D1 ;

hence g . x = (g1 union g2) . x ; :: thesis: verum

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;(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