deffunc H_{1}( 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_{1}(i)
from PBOOLE:sch 4();

for i being set st i in I holds

E . i is Relation of (M . i)

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

consider E being ManySortedSet of I such that

A1: for i being object st i in I holds

E . i = H

for i being set st i in I holds

E . i is Relation of (M . i)

proof

then reconsider E = E as ManySortedRelation of M by MSUALG_4:def 1;
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;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

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