let S be non empty non void ManySortedSign ; 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; 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; ( F is_monomorphism A,B implies A, Image F are_isomorphic )
assume A1:
F is_monomorphism A,B
; 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
; MSUALG_3:def 11 G is_isomorphism A, Image F
thus
G is_epimorphism A, Image F
by A3; MSUALG_3:def 10 G is_monomorphism A, Image F
thus
G is_homomorphism A, Image F
by A3; MSUALG_3:def 9 G is "1-1"
thus
G is "1-1"
by A1, A2; verum