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

( 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