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