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

for f being Element of MSAAut U1

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

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

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

let f be Element of MSAAut U1; :: thesis: for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

let g be Element of (MSAAutGroup U1); :: thesis: ( f = g implies f "" = g " )

consider g1 being Element of MSAAut U1 such that

A1: g1 = g " ;

assume f = g ; :: thesis: f "" = g "

then g1 ** f = g * (g ") by A1, Def6;

then g1 ** f = 1_ (MSAAutGroup U1) by GROUP_1:def 5;

then A2: g1 ** f = id the Sorts of U1 by Th29;

( f is "1-1" & f is "onto" ) by Lm3;

hence f "" = g " by A1, A2, Th17; :: thesis: verum

for f being Element of MSAAut U1

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

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

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

let f be Element of MSAAut U1; :: thesis: for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

let g be Element of (MSAAutGroup U1); :: thesis: ( f = g implies f "" = g " )

consider g1 being Element of MSAAut U1 such that

A1: g1 = g " ;

assume f = g ; :: thesis: f "" = g "

then g1 ** f = g * (g ") by A1, Def6;

then g1 ** f = 1_ (MSAAutGroup U1) by GROUP_1:def 5;

then A2: g1 ** f = id the Sorts of U1 by Th29;

( f is "1-1" & f is "onto" ) by Lm3;

hence f "" = g " by A1, A2, Th17; :: thesis: verum