let I, J be set ; :: thesis: for F1, F2 being ManySortedSet of
for G1, G2 being ManySortedSet of ex H1, H2 being ManySortedSet of st
( H1 = Intersect F1,G1 & H2 = Intersect F2,G2 & Intersect {|F1,F2|},{|G1,G2|} = {|H1,H2|} )
let F1, F2 be ManySortedSet of ; :: thesis: for G1, G2 being ManySortedSet of ex H1, H2 being ManySortedSet of st
( H1 = Intersect F1,G1 & H2 = Intersect F2,G2 & Intersect {|F1,F2|},{|G1,G2|} = {|H1,H2|} )
let G1, G2 be ManySortedSet of ; :: thesis: ex H1, H2 being ManySortedSet of st
( H1 = Intersect F1,G1 & H2 = Intersect F2,G2 & Intersect {|F1,F2|},{|G1,G2|} = {|H1,H2|} )
A1: [:(I /\ J),(I /\ J):] = [:I,I:] /\ [:J,J:] by ZFMISC_1:123;
then reconsider H1 = Intersect F1,G1, H2 = Intersect F2,G2 as ManySortedSet of by Th14;
take H1 ; :: thesis: ex H2 being ManySortedSet of 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|}
A2: ( dom F1 = [:I,I:] & dom G1 = [:J,J:] & dom H1 = [:(I /\ J),(I /\ J):] & dom F2 = [:I,I:] & dom G2 = [:J,J:] & dom H2 = [:(I /\ J),(I /\ J):] & dom {|F1,F2|} = [:I,I,I:] & dom {|G1,G2|} = [:J,J,J:] & dom {|H1,H2|} = [:(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 {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x) )
assume x in [:I,I,I:] /\ [:J,J,J:] ; :: thesis: {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . 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,b] in [:(I /\ J),(I /\ J):] & [b,c] in [:(I /\ J),(I /\ J):] ) by ZFMISC_1:106;
A9: ( {|F1,F2|} . a,b,c = [:(F2 . b,c),(F1 . a,b):] & {|G1,G2|} . a,b,c = [:(G2 . b,c),(G1 . a,b):] & {|H1,H2|} . a,b,c = [:(H2 . b,c),(H1 . a,b):] ) by A5, A6, A7, ALTCAT_1:def 6;
hence {|H1,H2|} . x = [:(H2 . b,c),(H1 . a,b):] by A5, MULTOP_1:def 1
.= [:((F2 . [b,c]) /\ (G2 . [b,c])),(H1 . a,b):] by A1, A2, A8, Def2
.= [:((F2 . [b,c]) /\ (G2 . [b,c])),((F1 . [a,b]) /\ (G1 . [a,b])):] by A1, A2, A8, Def2
.= [:(F2 . [b,c]),(F1 . [a,b]):] /\ [:(G2 . [b,c]),(G1 . [a,b]):] by ZFMISC_1:123
.= ({|F1,F2|} . x) /\ [:(G2 . [b,c]),(G1 . [a,b]):] by A5, A9, MULTOP_1:def 1
.= ({|F1,F2|} . x) /\ ({|G1,G2|} . x) by A5, A9, MULTOP_1:def 1 ;
:: thesis: verum

end;

hence Intersect {|F1,F2|},{|G1,G2|} = {|H1,H2|} by A2, A3, Def2; :: thesis: verum