for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )