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:]
A2: dom F c= dom f by A1, RELAT_1:60;
let G be PartFunc of [:Y2,Y2:],Y2; :: thesis: ( G = g || Y2 implies |:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A3: G = g || Y2 ; :: thesis: |:F,G:| = |:f,g:| || [:Y1,Y2:]
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: dom (|:f,g:| || [:Y1,Y2:]) c= dom |:F,G:|

proof

let x be object ; :: 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 object such that
A6: x = [[x11,x12],[x21,x22]] and
A7: [x11,x21] in dom F and
A8: [x12,x22] in dom G by Def3;
A9: x12 in Y2 by A8, ZFMISC_1:87;
A10: x22 in Y2 by A8, ZFMISC_1:87;
x21 in Y1 by A7, ZFMISC_1:87;
then A11: [x21,x22] in [:Y1,Y2:] by A10, ZFMISC_1:87;
x11 in Y1 by A7, ZFMISC_1:87;
then [x11,x12] in [:Y1,Y2:] by A9, ZFMISC_1:87;
then A12: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6, A11, ZFMISC_1:87;
x in dom |:f,g:| by A2, A4, A6, A7, A8, Def3;
then x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by A12, XBOOLE_0:def 4;
hence x in dom (|:f,g:| || [:Y1,Y2:]) by RELAT_1:61; :: thesis: verum

end;

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

end;

now :: thesis: for x being set st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x

let x be set ; :: thesis: ( x in dom |:F,G:| implies |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x )
assume A25: x in dom |:F,G:| ; :: thesis: |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x
then consider x11, x21, x12, x22 being object such that
A26: x = [[x11,x12],[x21,x22]] and
A27: [x11,x21] in dom F and
A28: [x12,x22] in dom G by Def3;
thus |:F,G:| . x = |:F,G:| . ([x11,x12],[x21,x22]) by A26
.= [(F . (x11,x21)),(G . (x12,x22))] by A27, A28, Def3
.= [(f . [x11,x21]),(G . [x12,x22])] by A1, A27, FUNCT_1:47
.= [(f . (x11,x21)),(g . (x12,x22))] by A3, A28, FUNCT_1:47
.= |:f,g:| . ([x11,x12],[x21,x22]) by A2, A4, A27, A28, Def3
.= (|:f,g:| || [:Y1,Y2:]) . x by A5, A25, A26, FUNCT_1:47 ; :: thesis: verum

end;

then A29: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x ;
thus |:F,G:| = |:f,g:| || [:Y1,Y2:] by A5, A29; :: thesis: verum