let S be non empty non void ManySortedSign ; :: thesis: for U1 being strict non-empty MSAlgebra of S ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
let U1 be strict non-empty MSAlgebra of S; :: thesis: ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
consider U0 being strict non-empty free MSAlgebra of S, F being ManySortedFunction of U0,U1 such that
A1: F is_epimorphism U0,U1 by Th19;
F is_homomorphism U0,U1 by A1, MSUALG_3:def 10;
then Image F = U1 by A1, MSUALG_3:19;
hence ex U0 being strict non-empty free MSAlgebra of S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 ) by A1; :: thesis: verum