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