let S be non empty non void ManySortedSign ; :: thesis: 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 b₂,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; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x1, x2 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,x1,x2) = Hom (T,x2,x1)
let X be V5() ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum