let I, J be set ; :: thesis: for F being ManySortedSet of
for G being ManySortedSet of ex H being ManySortedSet of st
( H = Intersect F,G & Intersect {|F|},{|G|} = {|H|} )
let F be ManySortedSet of ; :: thesis: for G being ManySortedSet of ex H being ManySortedSet of st
( H = Intersect F,G & Intersect {|F|},{|G|} = {|H|} )
let G be ManySortedSet of ; :: thesis: ex H being ManySortedSet of 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 by Th14;
take H ; :: thesis: ( H = Intersect F,G & Intersect {|F|},{|G|} = {|H|} )
thus H = Intersect F,G ; :: thesis: Intersect {|F|},{|G|} = {|H|}
A2: ( dom F = [:I,I:] & dom G = [:J,J:] & dom H = [:(I /\ J),(I /\ J):] & dom {|F|} = [:I,I,I:] & dom {|G|} = [:J,J,J:] & dom {|H|} = [:(I /\ J),(I /\ J),(I /\ J):] ) by PARTFUN1:def 4;
( [: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 A1, ZFMISC_1:123
.= [:(I /\ J),(I /\ J),(I /\ J):] by ZFMISC_1:def 3 ;

now

let x be set ; :: thesis: ( x in [:I,I,I:] /\ [:J,J,J:] implies {|H|} . x = ({|F|} . x) /\ ({|G|} . x) )
assume x in [:I,I,I:] /\ [:J,J,J:] ; :: thesis: {|H|} . x = ({|F|} . x) /\ ({|G|} . x)
then A4: ( x in [:I,I,I:] & x in [:J,J,J:] ) by XBOOLE_0:def 4;
then consider a, b, c being set such that
A5: ( a in I & b in I & c in I & x = [a,b,c] ) by MCART_1:72;
A6: ( a in J & b in J & c in J ) by A4, A5, MCART_1:73;
then A7: ( a in I /\ J & b in I /\ J & c in I /\ J ) by A5, XBOOLE_0:def 4;
then A8: [a,c] in [:(I /\ J),(I /\ J):] by ZFMISC_1:106;
A9: ( {|F|} . a,b,c = F . a,c & {|G|} . a,b,c = G . a,c & {|H|} . a,b,c = H . a,c ) by A5, A6, A7, ALTCAT_1:def 5;
hence {|H|} . x = H . [a,c] by A5, MULTOP_1:def 1
.= (F . a,c) /\ (G . [a,c]) by A1, A2, A8, Def2
.= ({|F|} . x) /\ (G . a,c) by A5, A9, MULTOP_1:def 1
.= ({|F|} . x) /\ ({|G|} . x) by A5, A9, MULTOP_1:def 1 ;
:: thesis: verum

end;

hence Intersect {|F|},{|G|} = {|H|} by A2, A3, Def2; :: thesis: verum