deffunc H₁( object ) -> set = (EqR1 (\/) EqR2) . $1;
consider E being ManySortedSet of I such that
A1: for i being object st i in I holds
E . i = H₁(i) from PBOOLE:sch 4();
for i being set st i in I holds
E . i is Relation of (M . i)

proof

let i be set ; :: thesis: ( i in I implies E . i is Relation of (M . i) )
assume A2: i in I ; :: thesis: E . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
E . i = (EqR1 (\/) EqR2) . i by A1, A2
.= (EqR1 . i9) \/ (EqR2 . i9) by PBOOLE:def 4 ;
hence E . i is Relation of (M . i) ; :: thesis: verum

end;

then reconsider E = E as ManySortedRelation of M by MSUALG_4:def 1;
take EqCl E ; :: thesis: ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 (\/) EqR2 & EqCl E = EqCl EqR3 )
take E ; :: thesis: ( E = EqR1 (\/) EqR2 & EqCl E = EqCl E )
thus ( E = EqR1 (\/) EqR2 & EqCl E = EqCl E ) by A1, PBOOLE:3; :: thesis: verum