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;

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

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)

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

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