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;

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)

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;

take H1 ; :: thesis: 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 ; :: 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