deffunc H1( Element of S) -> Element of K10(K11(( the Sorts of U1 . S),( the Sorts of U1 . S))) = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch 4();
 reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; :: thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume i in the carrier of S ; :: thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then f . i = id ( the Sorts of U1 . i) by A1;
hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; :: thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by Def1;
reconsider f = f as ManySortedRelation of U1 ;
take f ; :: thesis: f is MSEquivalence-like
for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; :: thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); :: thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume ( i in the carrier of S & f . i = R ) ; :: thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then R = id ( the Sorts of U1 . i) by A1;
hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; :: thesis: verum
end;
then f is MSEquivalence_Relation-like ;
hence f is MSEquivalence-like ; :: thesis: verum