let R be ManySortedRelation of A; :: thesis: ( R is MSEquivalence-like implies R is V2() )
assume A1: for i being set
for P being Relation of ( the Sorts of A . i) st i in the carrier of S & R . i = P holds
P is Equivalence_Relation of ( the Sorts of A . i) ; :: according to MSUALG_4:def 2,MSUALG_4:def 3 :: thesis: R is V2()
let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of S or not R . i is empty )
assume i in the carrier of S ; :: thesis: not R . i is empty
then reconsider i = i as SortSymbol of S ;
R . i is Equivalence_Relation of ( the Sorts of A . i) by A1;
hence not R . i is empty ; :: thesis: verum