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