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