let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
let A, B be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
let F be ManySortedFunction of A,B; :: thesis: ( F is_monomorphism A,B implies A, Image F are_isomorphic )
assume A1: F is_monomorphism A,B ; :: thesis: A, Image F are_isomorphic
then F is_homomorphism A,B ;
then consider G being ManySortedFunction of A,(Image F) such that
A2: G = F and
A3: G is_epimorphism A, Image F by MSUALG_3:21;
take G ; :: according to MSUALG_3:def 11 :: thesis: G is_isomorphism A, Image F
thus G is_epimorphism A, Image F by A3; :: according to MSUALG_3:def 10 :: thesis: G is_monomorphism A, Image F
thus G is_homomorphism A, Image F by A3; :: according to MSUALG_3:def 9 :: thesis: G is "1-1"
thus G is "1-1" by A1, A2; :: thesis: verum