let I, J be set ; :: thesis: 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:]; :: thesis: 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:]; :: thesis: 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;

( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

take H2 ; :: thesis: ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

thus ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) ) ; :: thesis: 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; :: thesis: verum

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:]; :: thesis: 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:]; :: thesis: 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 :: thesis: for x being object st x in [:I,I,I:] /\ [:J,J,J:] holds

{|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x)

take
H1
; :: thesis: ex H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x)

let x be object ; :: thesis: ( 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:] ; :: thesis: {|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 ;

:: thesis: verum

end;assume A6: x in [:I,I,I:] /\ [:J,J,J:] ; :: thesis: {|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 ;

:: thesis: verum

( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

take H2 ; :: thesis: ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )

thus ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) ) ; :: thesis: 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; :: thesis: verum