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:123;
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:123
.= [:(I /\ J),(I /\ J),(I /\ J):] by ZFMISC_1:def 3 ;
A3: ( dom F = [:I,I:] & dom G = [:J,J:] ) by PARTFUN1:def 4;

A4: now

let x be set ; :: 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 set 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:72;
A11: c in J by A6, A10, MCART_1:73;
then A12: c in I /\ J by A9, XBOOLE_0:def 4;
A13: a in J by A6, A10, MCART_1:73;
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:106;
A16: b in J by A6, A10, MCART_1:73;
then A17: {|G|} . a,b,c = G . a,c by A13, A11, ALTCAT_1:def 5;
A18: {|F|} . a,b,c = F . a,c by A7, A8, A9, ALTCAT_1:def 5;
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 5;
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 4;
( dom {|F|} = [:I,I,I:] & dom {|G|} = [:J,J,J:] ) by PARTFUN1:def 4;
hence Intersect {|F|},{|G|} = {|H|} by A19, A2, A4, Def2; :: thesis: verum