let I, J be set ; for F1, F2 being ManySortedSet of [:I,I:]
for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
let F1, F2 be ManySortedSet of [:I,I:]; for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
let G1, G2 be ManySortedSet of [:J,J:]; ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
A1:
( dom F2 = [:I,I:] & dom G2 = [:J,J:] )
by PARTFUN1:def 2;
A2:
[:(I /\ J),(I /\ J):] = [:I,I:] /\ [:J,J:]
by ZFMISC_1:100;
then reconsider H1 = Intersect (F1,G1), H2 = Intersect (F2,G2) as ManySortedSet of [:(I /\ J),(I /\ J):] by Th14;
( [:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:] )
by ZFMISC_1:def 3;
then A3: [:I,I,I:] /\ [:J,J,J:] =
[:[:(I /\ J),(I /\ J):],(I /\ J):]
by A2, ZFMISC_1:100
.=
[:(I /\ J),(I /\ J),(I /\ J):]
by ZFMISC_1:def 3
;
A4:
( dom F1 = [:I,I:] & dom G1 = [:J,J:] )
by PARTFUN1:def 2;
A5:
now for x being object st x in [:I,I,I:] /\ [:J,J,J:] holds
{|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x)let x be
object ;
( x in [:I,I,I:] /\ [:J,J,J:] implies {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x) )assume A6:
x in [:I,I,I:] /\ [:J,J,J:]
;
{|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x)then A7:
x in [:J,J,J:]
by XBOOLE_0:def 4;
x in [:I,I,I:]
by A6, XBOOLE_0:def 4;
then consider a,
b,
c being
object such that A8:
a in I
and A9:
b in I
and A10:
c in I
and A11:
x = [a,b,c]
by MCART_1:68;
A12:
b in J
by A7, A11, MCART_1:69;
then A13:
b in I /\ J
by A9, XBOOLE_0:def 4;
A14:
c in J
by A7, A11, MCART_1:69;
then A15:
c in I /\ J
by A10, XBOOLE_0:def 4;
then A16:
[b,c] in [:(I /\ J),(I /\ J):]
by A13, ZFMISC_1:87;
A17:
a in J
by A7, A11, MCART_1:69;
then A18:
a in I /\ J
by A8, XBOOLE_0:def 4;
then A19:
[a,b] in [:(I /\ J),(I /\ J):]
by A13, ZFMISC_1:87;
A20:
{|F1,F2|} . (
a,
b,
c)
= [:(F2 . (b,c)),(F1 . (a,b)):]
by A8, A9, A10, ALTCAT_1:def 4;
A21:
{|G1,G2|} . (
a,
b,
c)
= [:(G2 . (b,c)),(G1 . (a,b)):]
by A17, A12, A14, ALTCAT_1:def 4;
{|H1,H2|} . (
a,
b,
c)
= [:(H2 . (b,c)),(H1 . (a,b)):]
by A18, A13, A15, ALTCAT_1:def 4;
hence {|H1,H2|} . x =
[:(H2 . (b,c)),(H1 . (a,b)):]
by A11, MULTOP_1:def 1
.=
[:((F2 . [b,c]) /\ (G2 . [b,c])),(H1 . (a,b)):]
by A2, A1, A16, Def2
.=
[:((F2 . [b,c]) /\ (G2 . [b,c])),((F1 . [a,b]) /\ (G1 . [a,b])):]
by A2, A4, A19, Def2
.=
[:(F2 . [b,c]),(F1 . [a,b]):] /\ [:(G2 . [b,c]),(G1 . [a,b]):]
by ZFMISC_1:100
.=
({|F1,F2|} . x) /\ [:(G2 . [b,c]),(G1 . [a,b]):]
by A11, A20, MULTOP_1:def 1
.=
({|F1,F2|} . x) /\ ({|G1,G2|} . x)
by A11, A21, MULTOP_1:def 1
;
verum end;
take
H1
; ex H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
take
H2
; ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
thus
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) )
; Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|}
A22:
dom {|H1,H2|} = [:(I /\ J),(I /\ J),(I /\ J):]
by PARTFUN1:def 2;
( dom {|F1,F2|} = [:I,I,I:] & dom {|G1,G2|} = [:J,J,J:] )
by PARTFUN1:def 2;
hence
Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|}
by A22, A3, A5, Def2; verum