let I, J be set ; :: thesis: for A being ManySortedSet of
for B being ManySortedSet of holds Intersect A,B is ManySortedSet of
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of holds Intersect A,B is ManySortedSet of
let B be ManySortedSet of ; :: thesis: Intersect A,B is ManySortedSet of
( 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 by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum