let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),T holds
( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )
let X be V5() ManySortedSet of the carrier of S; for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),T holds
( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for h being ManySortedFunction of (Free (S,X)),T holds
( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )
let h be ManySortedFunction of (Free (S,X)),T; ( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )
canonical_homomorphism T is_homomorphism Free (S,X),T
by MSAFREE4:def 10;
hence
( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )
by HOMO; verum