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,x1,x2)) = id the Sorts of T
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,x1,x2)) = id the Sorts of T
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,x1,x2)) = id the Sorts of T
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,x1,x2)) = id the Sorts of T
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; (Hom (T,x1,x2)) ** (Hom (T,x1,x2)) = id the Sorts of T
set h = Hom (T,x1,x2);
for s being SortSymbol of S
for x being Element of X . s holds (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s) . (x -term) = x -term
proof
let s1 be
SortSymbol of
S;
for x being Element of X . s1 holds (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x -term) = x -term let x11 be
Element of
X . s1;
(((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term
A2:
(FreeGen T) . s1 c= the
Sorts of
T . s1
by PBOOLE:def 2, PBOOLE:def 18;
A3:
(
x11 -term in FreeGen (
s1,
X) &
FreeGen (
s1,
X)
= (FreeGen T) . s1 )
by MSAFREE:def 15, MSAFREE:def 16;
A4:
(((Hom (T,x1,x2)) . s1) * ((Hom (T,x1,x2)) . s1)) . (x11 -term) = ((Hom (T,x1,x2)) . s1) . (((Hom (T,x1,x2)) . s1) . (x11 -term))
by A2, A3, FUNCT_2:15;
per cases
( ( s1 = s & x11 = x1 ) or ( s1 = s & x11 = x2 ) or s1 <> s or ( x11 <> x1 & x11 <> x2 ) )
;
end;
end;
hence
(Hom (T,x1,x2)) ** (Hom (T,x1,x2)) = id the Sorts of T
by Th52; verum