let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x1,x2) = Hom (T,x2,x1)
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x1,x2) = Hom (T,x2,x1)
let X be V5() ManySortedSet of the carrier of S; for x1, x2 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,x1,x2) = Hom (T,x2,x1)
let x1, x2 be Element of X . s; for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x1,x2) = Hom (T,x2,x1)
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; Hom (T,x1,x2) = Hom (T,x2,x1)
( ((Hom (T,x2,x1)) . s) . (x1 -term) = x2 -term & ((Hom (T,x2,x1)) . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
((Hom (T,x2,x1)) . s1) . (y -term) = y -term ) )
by HOM;
hence
Hom (T,x1,x2) = Hom (T,x2,x1)
by HOM; verum