let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being MSAlgebra over S

for F being ManySortedFunction of U1,U2 holds

( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

let U1, U2 be MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 holds

( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

thus ( F is_isomorphism U1,U2 implies ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) :: thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" implies F is_isomorphism U1,U2 )

then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ;

hence F is_isomorphism U1,U2 ; :: thesis: verum

for F being ManySortedFunction of U1,U2 holds

( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

let U1, U2 be MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 holds

( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )

thus ( F is_isomorphism U1,U2 implies ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) :: thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" implies F is_isomorphism U1,U2 )

proof

assume
( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" )
; :: thesis: F is_isomorphism U1,U2
assume
F is_isomorphism U1,U2
; :: thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" )

then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ;

hence ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ; :: thesis: verum

end;then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ;

hence ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ; :: thesis: verum

then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ;

hence F is_isomorphism U1,U2 ; :: thesis: verum