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 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; :: thesis: 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; :: 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,x1,x2)) = id the Sorts of T
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,x1,x2)) = 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,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; :: thesis: 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; :: thesis: (((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 ) ) ;
suppose ( s1 = s & x11 = x1 ) ; :: thesis: (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term
then ( ((Hom (T,x1,x2)) . s1) . (x11 -term) = x2 -term & ((Hom (T,x1,x2)) . s1) . (x2 -term) = x11 -term ) by HOM;
hence (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term by A4, MSUALG_3:2; :: thesis: verum
end;
suppose ( s1 = s & x11 = x2 ) ; :: thesis: (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term
then ( ((Hom (T,x1,x2)) . s1) . (x11 -term) = x1 -term & ((Hom (T,x1,x2)) . s1) . (x1 -term) = x11 -term ) by HOM;
hence (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term by A4, MSUALG_3:2; :: thesis: verum
end;
suppose ( s1 <> s or ( x11 <> x1 & x11 <> x2 ) ) ; :: thesis: (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term
then ((Hom (T,x1,x2)) . s1) . (x11 -term) = x11 -term by HOM;
hence (((Hom (T,x1,x2)) ** (Hom (T,x1,x2))) . s1) . (x11 -term) = x11 -term by A4, MSUALG_3:2; :: thesis: verum
end;
end;
end;
hence (Hom (T,x1,x2)) ** (Hom (T,x1,x2)) = id the Sorts of T by Th52; :: thesis: verum