let A1, A2 be non empty set ; 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; 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; 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; 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; 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; ( 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
; 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; ( G = g || Y2 implies |:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A3:
G = g || Y2
; |: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:])
XBOOLE_0:def 10 dom (|:f,g:| || [:Y1,Y2:]) c= dom |:F,G:|proof
let x be
object ;
TARSKI:def 3 ( not x in dom |:F,G:| or x in dom (|:f,g:| || [:Y1,Y2:]) )
assume
x in dom |:F,G:|
;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( 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:])
;
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;
verum
end;
now for x being set st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . xlet x be
set ;
( x in dom |:F,G:| implies |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x )assume A25:
x in dom |:F,G:|
;
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . xthen 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
;
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; verum