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

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