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 4;
then dom (Intersect A,B) = I /\ J by Def2;
hence Intersect A,B is ManySortedSet of I /\ J by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum