let I, J be set ; :: thesis: 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:]; :: thesis: 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:]; :: thesis: 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 :: thesis: for x being object st x in [:I,I,I:] /\ [:J,J,J:] holds
{|H|} . x = ({|F|} . x) /\ ({|G|} . x)

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

end;

take H ; :: thesis: ( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
thus H = Intersect (F,G) ; :: thesis: 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; :: thesis: verum