let I, J be set ; :: thesis: for A being ManySortedSet of I

for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

let B be ManySortedSet of J; :: thesis: Intersect (A,B) is ManySortedSet of I /\ J

( dom A = I & dom B = J ) by PARTFUN1:def 2;

then dom (Intersect (A,B)) = I /\ J by Def2;

hence Intersect (A,B) is ManySortedSet of I /\ J by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum

for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J

let B be ManySortedSet of J; :: thesis: Intersect (A,B) is ManySortedSet of I /\ J

( dom A = I & dom B = J ) by PARTFUN1:def 2;

then dom (Intersect (A,B)) = I /\ J by Def2;

hence Intersect (A,B) is ManySortedSet of I /\ J by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum