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