let A1, A2 be non empty set ; :: thesis: for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let Y1 be non empty Subset of A1; :: thesis: for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let Y2 be non empty Subset of A2; :: thesis: for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let f be PartFunc of [:A1,A1:],A1; :: thesis: for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let g be PartFunc of [:A2,A2:],A2; :: thesis: for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let F be PartFunc of [:Y1,Y1:],Y1; :: thesis: ( F = f || Y1 implies for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A1: F = f || Y1 ; :: thesis: for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let G be PartFunc of [:Y2,Y2:],Y2; :: thesis: ( G = g || Y2 implies |:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A2: G = g || Y2 ; :: thesis: |:F,G:| = |:f,g:| || [:Y1,Y2:]
set X = dom |:F,G:|;
A3: ( dom F c= dom f & dom G c= dom g ) by A1, A2, RELAT_1:89;
A4: dom |:F,G:| c= [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:def 18;
A5: dom |:F,G:| = dom (|:f,g:| || [:Y1,Y2:])

proof

thus dom |:F,G:| c= dom (|:f,g:| || [:Y1,Y2:]) :: according to XBOOLE_0:def 10 :: thesis: dom (|:f,g:| || [:Y1,Y2:]) c= dom |:F,G:|

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom |:F,G:| or x in dom (|:f,g:| || [:Y1,Y2:]) )
assume x in dom |:F,G:| ; :: thesis: x in dom (|:f,g:| || [:Y1,Y2:])
then consider x11, x21, x12, x22 being set such that
A6: x = [[x11,x12],[x21,x22]] and
A7: [x11,x21] in dom F and
A8: [x12,x22] in dom G by FUNCT_4:def 3;
A9: x in dom |:f,g:| by A3, A6, A7, A8, FUNCT_4:def 3;
( dom F c= [:Y1,Y1:] & dom G c= [:Y2,Y2:] ) by A1, A2, RELAT_1:87;
then ( x11 in Y1 & x21 in Y1 & x12 in Y2 & x22 in Y2 ) by A7, A8, ZFMISC_1:106;
then ( [x11,x12] in [:Y1,Y2:] & [x21,x22] in [:Y1,Y2:] ) by ZFMISC_1:106;
then x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6, ZFMISC_1:106;
then x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by A9, XBOOLE_0:def 4;
hence x in dom (|:f,g:| || [:Y1,Y2:]) by RELAT_1:90; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (|:f,g:| || [:Y1,Y2:]) or x in dom |:F,G:| )
assume x in dom (|:f,g:| || [:Y1,Y2:]) ; :: thesis: x in dom |:F,G:|
then A10: x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:90;
then x in dom |:f,g:| by XBOOLE_0:def 4;
then consider x11, x21, x12, x22 being set such that
A11: x = [[x11,x12],[x21,x22]] and
A12: [x11,x21] in dom f and
A13: [x12,x22] in dom g by FUNCT_4:def 3;
x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A10, XBOOLE_0:def 4;
then ( [x11,x12] in [:Y1,Y2:] & [x21,x22] in [:Y1,Y2:] ) by A11, ZFMISC_1:106;
then ( x11 in Y1 & x12 in Y2 & x21 in Y1 & x22 in Y2 ) by ZFMISC_1:106;
then A14: ( [x11,x21] in [:Y1,Y1:] & [x12,x22] in [:Y2,Y2:] ) by ZFMISC_1:106;
( dom F = (dom f) /\ [:Y1,Y1:] & dom G = (dom g) /\ [:Y2,Y2:] ) by A1, A2, RELAT_1:90;
then ( [x11,x21] in dom F & [x12,x22] in dom G ) by A12, A13, A14, XBOOLE_0:def 4;
hence x in dom |:F,G:| by A11, FUNCT_4:def 3; :: thesis: verum

end;

A15: now

let x be set ; :: thesis: ( x in dom |:F,G:| implies |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x )
assume A16: x in dom |:F,G:| ; :: thesis: |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x
then consider x11, x21, x12, x22 being set such that
A17: x = [[x11,x12],[x21,x22]] and
A18: [x11,x21] in dom F and
A19: [x12,x22] in dom G by FUNCT_4:def 3;
thus |:F,G:| . x = |:F,G:| . [x11,x12],[x21,x22] by A17
.= [(F . x11,x21),(G . x12,x22)] by A18, A19, FUNCT_4:def 3
.= [(f . [x11,x21]),(G . [x12,x22])] by A1, A18, FUNCT_1:70
.= [(f . x11,x21),(g . x12,x22)] by A2, A19, FUNCT_1:70
.= |:f,g:| . [x11,x12],[x21,x22] by A3, A18, A19, FUNCT_4:def 3
.= (|:f,g:| || [:Y1,Y2:]) . x by A5, A16, A17, FUNCT_1:70 ; :: thesis: verum

end;

A20: rng (|:f,g:| || [:Y1,Y2:]) c= rng |:F,G:|

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (|:f,g:| || [:Y1,Y2:]) or x in rng |:F,G:| )
assume x in rng (|:f,g:| || [:Y1,Y2:]) ; :: thesis: x in rng |:F,G:|
then consider y being set such that
A21: y in dom (|:f,g:| || [:Y1,Y2:]) and
A22: x = (|:f,g:| || [:Y1,Y2:]) . y by FUNCT_1:def 5;
x = |:F,G:| . y by A5, A15, A21, A22;
hence x in rng |:F,G:| by A5, A21, FUNCT_1:def 5; :: thesis: verum

end;

A23: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x by A15;
rng |:F,G:| c= [:Y1,Y2:] by RELAT_1:def 19;
then rng (|:f,g:| || [:Y1,Y2:]) c= [:Y1,Y2:] by A20, XBOOLE_1:1;
then |:f,g:| || [:Y1,Y2:] is PartFunc of [:[:Y1,Y2:],[:Y1,Y2:]:],[:Y1,Y2:] by A4, A5, RELSET_1:11;
hence |:F,G:| = |:f,g:| || [:Y1,Y2:] by A5, A23, PARTFUN1:34; :: thesis: verum