let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1 holds f "" in MSAAut U1
let U1 be non-empty MSAlgebra of S; :: thesis: for f being Element of MSAAut U1 holds f "" in MSAAut U1
let f be Element of MSAAut U1; :: thesis: f "" in MSAAut U1
f is_isomorphism U1,U1 by Def7;
then f "" is_isomorphism U1,U1 by MSUALG_3:14;
hence f "" in MSAAut U1 by Def7; :: thesis: verum