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
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
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
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
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
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
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
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
let r be Element of T,s; :: thesis: ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r
the Sorts of T is MSSubset of (Free (S,X)) by MSAFREE4:def 6;
then A1: the Sorts of T . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
( (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r = (((Hom (T,x1,x2)) ** (canonical_homomorphism T)) . s) . r & (((Hom (T,x1,x2)) ** (canonical_homomorphism T)) . s) . r = (((Hom (T,x1,x2)) . s) * ((canonical_homomorphism T) . s)) . r & (((Hom (T,x1,x2)) . s) * ((canonical_homomorphism T) . s)) . r = ((Hom (T,x1,x2)) . s) . (((canonical_homomorphism T) . s) . r) & ((Hom (T,x1,x2)) . s) . (((canonical_homomorphism T) . s) . r) = ((Hom (T,x1,x2)) . s) . r ) by A1, Th66, MSUALG_3:2, FUNCT_2:15, MSAFREE4:47;
hence ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r ; :: thesis: verum