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

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

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

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

then reconsider AB = Intersect (A,B) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

I /\ I = I ;

then for i being object st i in I holds

AB . i = (A . i) /\ (B . i) by A1, Def2;

hence Intersect (A,B) = A (/\) B by PBOOLE:def 5; :: thesis: verum

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

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

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

then reconsider AB = Intersect (A,B) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

I /\ I = I ;

then for i being object st i in I holds

AB . i = (A . i) /\ (B . i) by A1, Def2;

hence Intersect (A,B) = A (/\) B by PBOOLE:def 5; :: thesis: verum