let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
let U1, U2 be non-empty MSAlgebra over S; for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
let F be ManySortedFunction of U1,U2; ( F is_homomorphism U1,U2 implies F is ManySortedFunction of U1,(Image F) )
assume A1:
F is_homomorphism U1,U2
; F is ManySortedFunction of U1,(Image F)
for i being object st i in the carrier of S holds
F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)
hence
F is ManySortedFunction of U1,(Image F)
by PBOOLE:def 15; verum