let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup U1)
let U1 be non-empty MSAlgebra over S; :: thesis: id the Sorts of U1 = 1_ (MSAAutGroup U1)
set T = the Sorts of U1;
set f = the Element of (MSAAutGroup U1);
reconsider g = id the Sorts of U1 as Element of (MSAAutGroup U1) by Th24;
consider g1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that
A1: g1 = g ;
the Element of (MSAAutGroup U1) is Element of MSAAut U1 ;
then consider f1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that
A2: f1 = the Element of (MSAAutGroup U1) ;
g * the Element of (MSAAutGroup U1) = f1 ** g1 by A1, A2, Def6
.= the Element of (MSAAutGroup U1) by A1, A2, MSUALG_3:3 ;
hence id the Sorts of U1 = 1_ (MSAAutGroup U1) by GROUP_1:7; :: thesis: verum