let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T
let x be Element of X . s; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: Hom (T,x,x) = id the Sorts of T
set h = Hom (T,x,x);
for s being SortSymbol of S
for x being Element of X . s holds ((Hom (T,x,x)) . s) . (x -term) = x -term

proof

let s1 be SortSymbol of S; :: thesis: for x being Element of X . s1 holds ((Hom (T,x,x)) . s1) . (x -term) = x -term
let x11 be Element of X . s1; :: thesis: ((Hom (T,x,x)) . s1) . (x11 -term) = x11 -term

per cases ( ( s1 = s & x11 = x ) or s1 <> s or x11 <> x ) ;

suppose ( s1 = s & x11 = x ) ; :: thesis: ((Hom (T,x,x)) . s1) . (x11 -term) = x11 -term

hence ((Hom (T,x,x)) . s1) . (x11 -term) = x11 -term by HOM; :: thesis: verum

end;

suppose ( s1 <> s or x11 <> x ) ; :: thesis: ((Hom (T,x,x)) . s1) . (x11 -term) = x11 -term

hence ((Hom (T,x,x)) . s1) . (x11 -term) = x11 -term by HOM; :: thesis: verum

end;

end;

end;

hence Hom (T,x,x) = id the Sorts of T by Th52; :: thesis: verum