let S be non empty non void ManySortedSign ; :: thesis: for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
let U1 be strict non-empty MSAlgebra over S; :: thesis: ex U0 being strict non-empty free MSAlgebra over 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 over S, F being ManySortedFunction of U0,U1 such that
A1: F is_epimorphism U0,U1 by Th18;
Image F = U1 by A1, MSUALG_3:19;
hence ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 ) by A1; :: thesis: verum