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

for f being Element of MSAAut U1 holds

( f is "1-1" & f is "onto" )

let U1 be non-empty MSAlgebra over S; :: thesis: for f being Element of MSAAut U1 holds

( f is "1-1" & f is "onto" )

let f be Element of MSAAut U1; :: thesis: ( f is "1-1" & f is "onto" )

f is_isomorphism U1,U1 by Def5;

hence ( f is "1-1" & f is "onto" ) by MSUALG_3:13; :: thesis: verum

for f being Element of MSAAut U1 holds

( f is "1-1" & f is "onto" )

let U1 be non-empty MSAlgebra over S; :: thesis: for f being Element of MSAAut U1 holds

( f is "1-1" & f is "onto" )

let f be Element of MSAAut U1; :: thesis: ( f is "1-1" & f is "onto" )

f is_isomorphism U1,U1 by Def5;

hence ( f is "1-1" & f is "onto" ) by MSUALG_3:13; :: thesis: verum