let A1, A2 be non empty set ; :: thesis:
let Y1 be non empty Subset of A1; :: thesis:
let Y2 be non empty Subset of A2; :: thesis:
let f be PartFunc of [:A1,A1:],A1; :: thesis:
let g be PartFunc of [:A2,A2:],A2; :: thesis:
let F be PartFunc of [:Y1,Y1:],Y1; :: thesis:
assume A1: F = f || Y1 ; :: thesis:
A2: dom F c= dom f by A1, RELAT_1:60;
let G be PartFunc of [:Y2,Y2:],Y2; :: thesis:
assume A3: G = g || Y2 ; :: thesis:
set X = dom |:F,G:|;
A4: dom G c= dom g by A3, RELAT_1:60;
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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in dom |:F,G:| ; :: thesis:
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: dom G c= [:Y2,Y2:] by A3, RELAT_1:58;
then A10: x12 in Y2 by A8, ZFMISC_1:87;
A11: x22 in Y2 by A8, A9, ZFMISC_1:87;
A12: dom F c= [:Y1,Y1:] by A1, RELAT_1:58;
then x21 in Y1 by A7, ZFMISC_1:87;
then A13: [x21,x22] in [:Y1,Y2:] by A11, ZFMISC_1:87;
x11 in Y1 by A7, A12, ZFMISC_1:87;
then [x11,x12] in [:Y1,Y2:] by A10, ZFMISC_1:87;
then A14: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6, A13, ZFMISC_1:87;
x in dom |:f,g:| by A2, A4, A6, A7, A8, FUNCT_4:def 3;
then x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by A14, XBOOLE_0:def 4;
hence x in dom (|:f,g:| || [:Y1,Y2:]) by RELAT_1:61; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
A15: dom F = (dom f) /\ [:Y1,Y1:] by A1, RELAT_1:61;
assume x in dom (|:f,g:| || [:Y1,Y2:]) ; :: thesis:
then A16: x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:61;
then A17: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by XBOOLE_0:def 4;
A18: dom G = (dom g) /\ [:Y2,Y2:] by A3, RELAT_1:61;
x in dom |:f,g:| by A16, XBOOLE_0:def 4;
then consider x11, x21, x12, x22 being set such that
A19: x = [[x11,x12],[x21,x22]] and
A20: [x11,x21] in dom f and
A21: [x12,x22] in dom g by FUNCT_4:def 3;
A22: [x21,x22] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87;
then A23: x22 in Y2 by ZFMISC_1:87;
A24: [x11,x12] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87;
then x12 in Y2 by ZFMISC_1:87;
then [x12,x22] in [:Y2,Y2:] by A23, ZFMISC_1:87;
then A25: [x12,x22] in dom G by A21, A18, XBOOLE_0:def 4;
A26: x21 in Y1 by A22, ZFMISC_1:87;
x11 in Y1 by A24, ZFMISC_1:87;
then [x11,x21] in [:Y1,Y1:] by A26, ZFMISC_1:87;
then [x11,x21] in dom F by A20, A15, XBOOLE_0:def 4;
hence x in dom |:F,G:| by A19, A25, FUNCT_4:def 3; :: thesis:

end;

A27: now

let x be set ; :: thesis:
assume A28: x in dom |:F,G:| ; :: thesis:
then consider x11, x21, x12, x22 being set such that
A29: x = [[x11,x12],[x21,x22]] and
A30: [x11,x21] in dom F and
A31: [x12,x22] in dom G by FUNCT_4:def 3;
thus |:F,G:| . x = |:F,G:| . ([x11,x12],[x21,x22]) by A29
.= [(F . (x11,x21)),(G . (x12,x22))] by A30, A31, FUNCT_4:def 3
.= [(f . [x11,x21]),(G . [x12,x22])] by A1, A30, FUNCT_1:47
.= [(f . (x11,x21)),(g . (x12,x22))] by A3, A31, FUNCT_1:47
.= |:f,g:| . ([x11,x12],[x21,x22]) by A2, A4, A30, A31, FUNCT_4:def 3
.= (|:f,g:| || [:Y1,Y2:]) . x by A5, A28, A29, FUNCT_1:47 ; :: thesis:

end;

then A32: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x ;
A33: rng (|:f,g:| || [:Y1,Y2:]) c= rng |:F,G:|

proof

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

end;

A36: dom |:F,G:| c= [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:def 18;
rng |:F,G:| c= [:Y1,Y2:] by RELAT_1:def 19;
then rng (|:f,g:| || [:Y1,Y2:]) c= [:Y1,Y2:] by A33, XBOOLE_1:1;
then |:f,g:| || [:Y1,Y2:] is PartFunc of [:[:Y1,Y2:],[:Y1,Y2:]:],[:Y1,Y2:] by A36, A5, RELSET_1:4;
hence |:F,G:| = |:f,g:| || [:Y1,Y2:] by A5, A32, PARTFUN1:5; :: thesis: