deffunc H₁( Element of S) -> Element of K6(K7((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 = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in dom f holds
f . x is Relation

proof

let x be set ; :: thesis: ( x in dom f implies f . x is Relation )
assume x in dom f ; :: thesis: f . x is Relation
then f . x = id (the Sorts of U1 . x) by A1;
hence f . x is Relation ; :: thesis: verum

end;

then reconsider f = f as ManySortedRelation of the carrier of S by Def1;
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 Def2;
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 by Def3;
hence f is MSEquivalence-like by Def5; :: thesis: verum