:: AUTGROUP semantic presentation

Lemma1: for b1 being strict Group
for b2 being Subgroup of b1 holds
( ( for b3, b4 being Element of b1 holds
( b4 is Element of b2 implies b4 |^ b3 in b2 ) ) implies b2 is normal )
proof
let c1 be strict Group;
let c2 be Subgroup of c1;
assume E2: for b1, b2 being Element of c1 holds
( b2 is Element of c2 implies b2 |^ b1 in c2 ) ;
now
let c3 be Element of c1;
thus c2 * c3 c= c3 * c2
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in c2 * c3 ;
then consider c5 being Element of c1 such that
E3: c4 = c5 * c3 and
E4: c5 in c2 by GROUP_2:126;
set c6 = carr c2;
c5 is Element of c2 by E4, RLVECT_1:def 1;
then c5 |^ c3 in c2 by E2;
then c5 |^ c3 in carr c2 by RLVECT_1:def 1;
then ((c3 " ) * c5) * c3 in carr c2 ;
then c3 * (((c3 " ) * c5) * c3) in c3 * (carr c2) by GROUP_2:33;
then c3 * ((c3 " ) * (c5 * c3)) in c3 * (carr c2) by GROUP_1:def 4;
then (c3 * (c3 " )) * (c5 * c3) in c3 * (carr c2) by GROUP_1:def 4;
then ((c3 * (c3 " )) * c5) * c3 in c3 * (carr c2) by GROUP_1:def 4;
then ((1. c1) * c5) * c3 in c3 * (carr c2) by GROUP_1:def 6;
then c4 in c3 * (carr c2) by E3, GROUP_1:def 5;
hence c4 in c3 * c2 ;
end;
end;
hence c2 is normal by GROUP_3:142;
end;

Lemma2: for b1 being strict Group
for b2 being Subgroup of b1 holds
( b2 is normal implies for b3, b4 being Element of b1 holds
( b4 is Element of b2 implies b4 |^ b3 in b2 ) )
proof
let c1 be strict Group;
let c2 be Subgroup of c1;
assume E3: c2 is normal ;
let c3, c4 be Element of c1;
assume E4: c4 is Element of c2 ;
set c5 = carr c2;
consider c6 being set such that
E5: c6 = c4 ;
c6 in c2 by E4, E5, RLVECT_1:def 1;
then E6: ( c4 in carr c2 & c4 in c2 ) by E5, RLVECT_1:def 1;
c2 * c3 = c3 * c2 by E3, GROUP_3:140;
then ((c3 " ) * c2) * c3 = (c3 " ) * (c3 * c2) by GROUP_2:128;
then ((c3 " ) * c2) * c3 = ((c3 " ) * c3) * c2 by GROUP_2:127;
then ((c3 " ) * c2) * c3 = (1. c1) * c2 by GROUP_1:def 6;
then ((c3 " ) * c2) * c3 = carr c2 by GROUP_2:132;
then the carrier of (c2 |^ c3) = carr c2 by GROUP_3:71;
then E7: (carr c2) |^ c3 = carr c2 by GROUP_3:def 6;
(c3 " ) * c4 in (c3 " ) * (carr c2) by E6, GROUP_2:33;
then ((c3 " ) * c4) * c3 in ((c3 " ) * (carr c2)) * c3 by GROUP_2:34;
then c4 |^ c3 in ((c3 " ) * (carr c2)) * c3 ;
then c4 |^ c3 in carr c2 by E7, GROUP_3:59;
hence c4 |^ c3 in c2 by RLVECT_1:def 1;
end;

theorem Th1: :: AUTGROUP:1
for b1 being strict Group
for b2 being Subgroup of b1 holds
( ( for b3, b4 being Element of b1 holds
( b4 is Element of b2 implies b4 |^ b3 in b2 ) ) iff b2 is normal ) by Lemma1, Lemma2;

definition
let c1 be strict Group;
func Aut c1 -> FUNCTION_DOMAIN of the carrier of a1,the carrier of a1 means :Def1: :: AUTGROUP:def 1
( ( for b1 being Element of a2 holds
b1 is Homomorphism of a1,a1 ) & ( for b1 being Homomorphism of a1,a1 holds
( b1 in a2 iff ( b1 is one-to-one & b1 is_epimorphism ) ) ) );
existence
ex b1 being FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 st
( ( for b2 being Element of b1 holds
b2 is Homomorphism of c1,c1 ) & ( for b2 being Homomorphism of c1,c1 holds
( b2 in b1 iff ( b2 is one-to-one & b2 is_epimorphism ) ) ) )
proof
set c2 = { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Homomorphism of c1,c1 st
( b1 = b2 & b2 is one-to-one & b2 is_epimorphism ) } ;
E3: id the carrier of c1 in { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Homomorphism of c1,c1 st
( b1 = b2 & b2 is one-to-one & b2 is_epimorphism ) }
proof
set c3 = id the carrier of c1;
E4: id the carrier of c1 in Funcs the carrier of c1,the carrier of c1 by FUNCT_2:11;
reconsider c4 = id the carrier of c1 as Homomorphism of c1,c1 by GROUP_6:47;
rng c4 = the carrier of c1 by RELAT_1:71;
then c4 is_epimorphism by GROUP_6:def 13;
hence id the carrier of c1 in { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Homomorphism of c1,c1 st
( b1 = b2 & b2 is one-to-one & b2 is_epimorphism ) } by E4;
end;
reconsider c3 = { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Homomorphism of c1,c1 st
( b1 = b2 & b2 is one-to-one & b2 is_epimorphism ) } as set ;
c3 is functional
proof
let c4 be set ; :: according to FRAENKEL:def 1
assume c4 in c3 ;
then consider c5 being Element of Funcs the carrier of c1,the carrier of c1 such that
E4: ( c4 = c5 & ex b1 being Homomorphism of c1,c1 st
( b1 = c5 & b1 is one-to-one & b1 is_epimorphism ) ) ;
thus c4 is Function by E4;
end;
then reconsider c4 = c3 as non empty functional set by E3;
c4 is FUNCTION_DOMAIN of the carrier of c1,the carrier of c1
proof
let c5 be Element of c4; :: according to FRAENKEL:def 2
c5 in c4 ;
then consider c6 being Element of Funcs the carrier of c1,the carrier of c1 such that
E4: ( c5 = c6 & ex b1 being Homomorphism of c1,c1 st
( b1 = c6 & b1 is one-to-one & b1 is_epimorphism ) ) ;
thus c5 is Function of the carrier of c1,the carrier of c1 by E4;
end;
then reconsider c5 = c4 as FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 ;
take c5 ;
hereby
let c6 be Element of c5;
c6 in c5 ;
then ex b1 being Element of Funcs the carrier of c1,the carrier of c1 st
( c6 = b1 & ex b2 being Homomorphism of c1,c1 st
( b2 = b1 & b2 is one-to-one & b2 is_epimorphism ) ) ;
hence c6 is Homomorphism of c1,c1 ;
end;
let c6 be Homomorphism of c1,c1;
hereby
assume c6 in c5 ;
then ex b1 being Element of Funcs the carrier of c1,the carrier of c1 st
( b1 = c6 & ex b2 being Homomorphism of c1,c1 st
( b2 = b1 & b2 is one-to-one & b2 is_epimorphism ) ) ;
hence ( c6 is one-to-one & c6 is_epimorphism ) ;
end;
assume E4: ( c6 is one-to-one & c6 is_epimorphism ) ;
c6 is Element of Funcs the carrier of c1,the carrier of c1 by FUNCT_2:11;
hence c6 in c5 by E4;
end;
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 holds
( ( for b3 being Element of b1 holds
b3 is Homomorphism of c1,c1 ) & ( for b3 being Homomorphism of c1,c1 holds
( b3 in b1 iff ( b3 is one-to-one & b3 is_epimorphism ) ) ) & ( for b3 being Element of b2 holds
b3 is Homomorphism of c1,c1 ) & ( for b3 being Homomorphism of c1,c1 holds
( b3 in b2 iff ( b3 is one-to-one & b3 is_epimorphism ) ) ) implies b1 = b2 )
proof
let c2, c3 be FUNCTION_DOMAIN of the carrier of c1,the carrier of c1;
assume that
E3: ( ( for b1 being Element of c2 holds
b1 is Homomorphism of c1,c1 ) & ( for b1 being Homomorphism of c1,c1 holds
( b1 in c2 iff ( b1 is one-to-one & b1 is_epimorphism ) ) ) ) and
E4: ( ( for b1 being Element of c3 holds
b1 is Homomorphism of c1,c1 ) & ( for b1 being Homomorphism of c1,c1 holds
( b1 in c3 iff ( b1 is one-to-one & b1 is_epimorphism ) ) ) ) ;
E5: c2 c= c3
proof
let c4 be set ; :: according to TARSKI:def 3
assume E6: c4 in c2 ;
then reconsider c5 = c4 as Homomorphism of c1,c1 by E3;
( c5 is one-to-one & c5 is_epimorphism ) by E3, E6;
hence c4 in c3 by E4;
end;
c3 c= c2
proof
let c4 be set ; :: according to TARSKI:def 3
assume E6: c4 in c3 ;
then reconsider c5 = c4 as Homomorphism of c1,c1 by E4;
( c5 is one-to-one & c5 is_epimorphism ) by E4, E6;
hence c4 in c2 by E3;
end;
hence c2 = c3 by E5, XBOOLE_0:def 10;
end;
end;

:: deftheorem Def1 defines Aut AUTGROUP:def 1 :
for b1 being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of b1,the carrier of b1 holds
( b2 = Aut b1 iff ( ( for b3 being Element of b2 holds
b3 is Homomorphism of b1,b1 ) & ( for b3 being Homomorphism of b1,b1 holds
( b3 in b2 iff ( b3 is one-to-one & b3 is_epimorphism ) ) ) ) );

theorem Th2: :: AUTGROUP:2
canceled;

theorem Th3: :: AUTGROUP:3
for b1 being strict Group holds Aut b1 c= Funcs the carrier of b1,the carrier of b1
proof
let c1 be strict Group;
let c2 be set ; :: according to TARSKI:def 3
assume c2 in Aut c1 ;
then consider c3 being Element of Aut c1 such that
E4: c3 = c2 ;
thus c2 in Funcs the carrier of c1,the carrier of c1 by E4, FUNCT_2:12;
end;

theorem Th4: :: AUTGROUP:4
for b1 being strict Group holds
id the carrier of b1 is Element of Aut b1
proof
let c1 be strict Group;
id the carrier of c1 is Homomorphism of c1,c1 by GROUP_6:47;
then consider c2 being Homomorphism of c1,c1 such that
E5: c2 = id the carrier of c1 ;
c2 is_epimorphism
proof
rng c2 = the carrier of c1 by E5, RELAT_1:71;
hence c2 is_epimorphism by GROUP_6:def 13;
end;
hence id the carrier of c1 is Element of Aut c1 by E5, Def1;
end;

theorem Th5: :: AUTGROUP:5
for b1 being strict Group
for b2 being Homomorphism of b1,b1 holds
( b2 in Aut b1 iff b2 is_isomorphism )
proof
let c1 be strict Group;
let c2 be Homomorphism of c1,c1;
hereby
assume E6: c2 in Aut c1 ;
then E7: c2 is_epimorphism by Def1;
c2 is one-to-one by E6, Def1;
then c2 is_monomorphism by GROUP_6:def 12;
hence c2 is_isomorphism by E7, GROUP_6:def 14;
end;
hereby
assume c2 is_isomorphism ;
then E6: ( c2 is_epimorphism & c2 is_monomorphism ) by GROUP_6:def 14;
then c2 is one-to-one by GROUP_6:def 12;
hence c2 in Aut c1 by E6, Def1;
end;
end;

Lemma6: for b1 being strict Group
for b2 being Element of Aut b1 holds
( dom b2 = rng b2 & dom b2 = the carrier of b1 )
proof
let c1 be strict Group;
let c2 be Element of Aut c1;
reconsider c3 = c2 as Homomorphism of c1,c1 by Def1;
c3 is_isomorphism by Th5;
then ( dom c3 = the carrier of c1 & rng c3 = the carrier of c1 ) by GROUP_6:71;
hence ( dom c2 = rng c2 & dom c2 = the carrier of c1 ) ;
end;

theorem Th6: :: AUTGROUP:6
for b1 being strict Group
for b2 being Element of Aut b1 holds
b2 " is Homomorphism of b1,b1
proof
let c1 be strict Group;
let c2 be Element of Aut c1;
reconsider c3 = c2 as Homomorphism of c1,c1 by Def1;
c3 is_isomorphism by Th5;
hence c2 " is Homomorphism of c1,c1 by GROUP_6:72;
end;

theorem Th7: :: AUTGROUP:7
for b1 being strict Group
for b2 being Element of Aut b1 holds
b2 " is Element of Aut b1
proof
let c1 be strict Group;
let c2 be Element of Aut c1;
reconsider c3 = c2 as Homomorphism of c1,c1 by Def1;
E9: c3 is_isomorphism by Th5;
reconsider c4 = c3 " as Homomorphism of c1,c1 by Th6;
c4 is_isomorphism by E9, GROUP_6:73;
then E10: ( c4 is_epimorphism & c4 is_monomorphism ) by GROUP_6:def 14;
then c4 is one-to-one by GROUP_6:def 12;
hence c2 " is Element of Aut c1 by E10, Def1;
end;

theorem Th8: :: AUTGROUP:8
for b1 being strict Group
for b2, b3 being Element of Aut b1 holds
b2 * b3 is Element of Aut b1
proof
let c1 be strict Group;
let c2, c3 be Element of Aut c1;
reconsider c4 = c2, c5 = c3 as Homomorphism of c1,c1 by Def1;
( c4 is_isomorphism & c5 is_isomorphism ) by Th5;
then c4 * c5 is_isomorphism by GROUP_6:74;
hence c2 * c3 is Element of Aut c1 by Th5;
end;

definition
let c1 be strict Group;
func AutComp c1 -> BinOp of Aut a1 means :Def2: :: AUTGROUP:def 2
for b1, b2 being Element of Aut a1 holds a2 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of Aut c1 st
for b2, b3 being Element of Aut c1 holds b1 . b2,b3 = b2 * b3
proof
defpred S1[ Element of Aut c1, Element of Aut c1, set ] means a3 = a1 * a2;
E10: for b1, b2 being Element of Aut c1 holds
ex b3 being Element of Aut c1 st
S1[b1,b2,b3]
proof
let c2, c3 be Element of Aut c1;
reconsider c4 = c2, c5 = c3 as Homomorphism of c1,c1 by Def1;
reconsider c6 = c4 * c5 as Element of Aut c1 by Th8;
take c6 ;
thus S1[c2,c3,c6] ;
end;
thus ex b1 being BinOp of Aut c1 st
for b2, b3 being Element of Aut c1 holds
S1[b2,b3,b1 . b2,b3] from BINOP_1:sch 3(E10);
end;
uniqueness
for b1, b2 being BinOp of Aut c1 holds
( ( for b3, b4 being Element of Aut c1 holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of Aut c1 holds b2 . b3,b4 = b3 * b4 ) implies b1 = b2 )
proof
let c2, c3 be BinOp of Aut c1;
assume that
E10: for b1, b2 being Element of Aut c1 holds c2 . b1,b2 = b1 * b2 and
E11: for b1, b2 being Element of Aut c1 holds c3 . b1,b2 = b1 * b2 ;
for b1, b2 being Element of Aut c1 holds c2 . b1,b2 = c3 . b1,b2
proof
let c4, c5 be Element of Aut c1;
thus c2 . c4,c5 = c4 * c5 by E10
.= c3 . c4,c5 by E11 ;
end;
hence c2 = c3 by BINOP_1:2;
end;
end;

:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
for b1 being strict Group
for b2 being BinOp of Aut b1 holds
( b2 = AutComp b1 iff for b3, b4 being Element of Aut b1 holds b2 . b3,b4 = b3 * b4 );

definition
let c1 be strict Group;
func AutGroup c1 -> strict Group equals :: AUTGROUP:def 3
 HGrStr(# (Aut a1),(AutComp a1) #);
coherence
HGrStr(# (Aut c1),(AutComp c1) #) is strict Group
proof
set c2 = HGrStr(# (Aut c1),(AutComp c1) #);
( HGrStr(# (Aut c1),(AutComp c1) #) is associative & HGrStr(# (Aut c1),(AutComp c1) #) is Group-like )
proof
E11: for b1, b2 being Element of HGrStr(# (Aut c1),(AutComp c1) #)
for b3, b4 being Element of Aut c1 holds
( b1 = b3 & b2 = b4 implies b1 * b2 = b3 * b4 ) by Def2;
thus for b1, b2, b3 being Element of HGrStr(# (Aut c1),(AutComp c1) #) holds (b1 * b2) * b3 = b1 * (b2 * b3) :: according to GROUP_1:def 4
proof
let c3, c4, c5 be Element of HGrStr(# (Aut c1),(AutComp c1) #);
reconsider c6 = c3, c7 = c4, c8 = c5 as Element of Aut c1 ;
E12: c3 * c4 = c6 * c7 by E11;
E13: c4 * c5 = c7 * c8 by E11;
thus (c3 * c4) * c5 = (c6 * c7) * c8 by E11, E12
.= c6 * (c7 * c8) by RELAT_1:55
.= c3 * (c4 * c5) by E11, E13 ;
end;
thus ex b1 being Element of HGrStr(# (Aut c1),(AutComp c1) #) st
for b2 being Element of HGrStr(# (Aut c1),(AutComp c1) #) holds
( b2 * b1 = b2 & b1 * b2 = b2 & ex b3 being Element of HGrStr(# (Aut c1),(AutComp c1) #) st
( b2 * b3 = b1 & b3 * b2 = b1 ) ) :: according to GROUP_1:def 3
proof
reconsider c3 = id the carrier of c1 as Element of HGrStr(# (Aut c1),(AutComp c1) #) by Th4;
take c3 ;
let c4 be Element of HGrStr(# (Aut c1),(AutComp c1) #);
consider c5 being Element of Aut c1 such that
E12: c5 = c4 ;
c4 * c3 = c5 * (id the carrier of c1) by E11, E12
.= c5 by FUNCT_2:23 ;
hence c4 * c3 = c4 by E12;
c3 * c4 = (id the carrier of c1) * c5 by E11, E12
.= c5 by FUNCT_2:23 ;
hence c3 * c4 = c4 by E12;
reconsider c6 = c5 " as Element of HGrStr(# (Aut c1),(AutComp c1) #) by Th7;
take c6 ;
reconsider c7 = c5 as Homomorphism of c1,c1 by Def1;
E13: ( c7 is one-to-one & c7 is_epimorphism ) by Def1;
then E14: rng c7 = the carrier of c1 by GROUP_6:def 13;
thus c4 * c6 = c7 * (c7 " ) by E11, E12
.= c3 by E13, E14, FUNCT_2:35 ;
thus c6 * c4 = (c7 " ) * c7 by E11, E12
.= c3 by E13, E14, FUNCT_2:35 ;
end;
end;
hence HGrStr(# (Aut c1),(AutComp c1) #) is strict Group ;
end;
end;

:: deftheorem Def3 defines AutGroup AUTGROUP:def 3 :
for b1 being strict Group holds AutGroup b1 = HGrStr(# (Aut b1),(AutComp b1) #);

theorem Th9: :: AUTGROUP:9
for b1 being strict Group
for b2, b3 being Element of (AutGroup b1)
for b4, b5 being Element of Aut b1 holds
( b2 = b4 & b3 = b5 implies b2 * b3 = b4 * b5 ) by Def2;

theorem Th10: :: AUTGROUP:10
for b1 being strict Group holds id the carrier of b1 = 1. (AutGroup b1)
proof
let c1 be strict Group;
reconsider c2 = id the carrier of c1 as Element of (AutGroup c1) by Th4;
consider c3 being Function of the carrier of c1,the carrier of c1 such that
E13: c3 = c2 ;
consider c4 being Element of (AutGroup c1);
c4 is Homomorphism of c1,c1 by Def1;
then consider c5 being Function of the carrier of c1,the carrier of c1 such that
E14: c5 = c4 ;
E15: c5 * c3 = c5 by E13, FUNCT_2:23;
( c5 = c4 & c3 = c2 implies c5 * c3 = c4 * c2 ) by Th9;
hence id the carrier of c1 = 1. (AutGroup c1) by E13, E14, E15, GROUP_1:15;
end;

theorem Th11: :: AUTGROUP:11
for b1 being strict Group
for b2 being Element of Aut b1
for b3 being Element of (AutGroup b1) holds
( b2 = b3 implies b2 " = b3 " )
proof
let c1 be strict Group;
let c2 be Element of Aut c1;
let c3 be Element of (AutGroup c1);
assume E14: c2 = c3 ;
consider c4 being Element of Aut c1 such that
E15: c4 = c3 " ;
E16: rng c2 = dom c2 by Lemma6
.= the carrier of c1 by Lemma6 ;
c2 is Homomorphism of c1,c1 by Def1;
then E17: c2 is one-to-one by Def1;
c4 * c2 = (c3 " ) * c3 by E14, E15, Th9;
then c4 * c2 = 1. (AutGroup c1) by GROUP_1:def 6;
then c4 * c2 = id the carrier of c1 by Th10;
hence c2 " = c3 " by E15, E16, E17, FUNCT_2:36;
end;

definition
let c1 be strict Group;
func InnAut c1 -> FUNCTION_DOMAIN of the carrier of a1,the carrier of a1 means :Def4: :: AUTGROUP:def 4
for b1 being Element of Funcs the carrier of a1,the carrier of a1 holds
( b1 in a2 iff ex b2 being Element of a1 st
for b3 being Element of a1 holds b1 . b3 = b3 |^ b2 );
existence
ex b1 being FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 st
for b2 being Element of Funcs the carrier of c1,the carrier of c1 holds
( b2 in b1 iff ex b3 being Element of c1 st
for b4 being Element of c1 holds b2 . b4 = b4 |^ b3 )
proof
set c2 = { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Element of c1 st
for b2 being Element of c1 holds b1 . b3 = b3 |^ b2 } ;
set c3 = id the carrier of c1;
E14: id the carrier of c1 is Element of Funcs the carrier of c1,the carrier of c1 by FUNCT_2:11;
ex b1 being Element of c1 st
for b2 being Element of c1 holds (id the carrier of c1) . b2 = b2 |^ b1
proof
take c4 = 1. c1;
let c5 be Element of c1;
E15: c4 " = 1. c1 by GROUP_1:16;
thus (id the carrier of c1) . c5 = c5 by FUNCT_1:35
.= c5 * c4 by GROUP_1:def 5
.= ((c4 " ) * c5) * c4 by E15, GROUP_1:def 5
.= c5 |^ c4 ;
end;
then E15: id the carrier of c1 in { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Element of c1 st
for b2 being Element of c1 holds b1 . b3 = b3 |^ b2 } by E14;
{ b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Element of c1 st
for b2 being Element of c1 holds b1 . b3 = b3 |^ b2 } is functional
proof
let c4 be set ; :: according to FRAENKEL:def 1
assume c4 in { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Element of c1 st
for b2 being Element of c1 holds b1 . b3 = b3 |^ b2 } ;
then ex b1 being Element of Funcs the carrier of c1,the carrier of c1 st
( b1 = c4 & ex b2 being Element of c1 st
for b3 being Element of c1 holds b1 . b3 = b3 |^ b2 ) ;
hence c4 is Function ;
end;
then reconsider c4 = { b1 where B is Element of Funcs the carrier of c1,the carrier of c1 : ex b1 being Element of c1 st
for b2 being Element of c1 holds b1 . b3 = b3 |^ b2 } as non empty functional set by E15;
c4 is FUNCTION_DOMAIN of the carrier of c1,the carrier of c1
proof
let c5 be Element of c4; :: according to FRAENKEL:def 2
c5 in c4 ;
then ex b1 being Element of Funcs the carrier of c1,the carrier of c1 st
( b1 = c5 & ex b2 being Element of c1 st
for b3 being Element of c1 holds b1 . b3 = b3 |^ b2 ) ;
hence c5 is Function of the carrier of c1,the carrier of c1 ;
end;
then reconsider c5 = c4 as FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 ;
take c5 ;
let c6 be Element of Funcs the carrier of c1,the carrier of c1;
hereby
assume c6 in c5 ;
then ex b1 being Element of Funcs the carrier of c1,the carrier of c1 st
( b1 = c6 & ex b2 being Element of c1 st
for b3 being Element of c1 holds b1 . b3 = b3 |^ b2 ) ;
hence ex b1 being Element of c1 st
for b2 being Element of c1 holds c6 . b2 = b2 |^ b1 ;
end;
thus ( ex b1 being Element of c1 st
for b2 being Element of c1 holds c6 . b2 = b2 |^ b1 implies c6 in c5 ) ;
end;
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of c1,the carrier of c1 holds
( ( for b3 being Element of Funcs the carrier of c1,the carrier of c1 holds
( b3 in b1 iff ex b4 being Element of c1 st
for b5 being Element of c1 holds b3 . b5 = b5 |^ b4 ) ) & ( for b3 being Element of Funcs the carrier of c1,the carrier of c1 holds
( b3 in b2 iff ex b4 being Element of c1 st
for b5 being Element of c1 holds b3 . b5 = b5 |^ b4 ) ) implies b1 = b2 )
proof
let c2, c3 be FUNCTION_DOMAIN of the carrier of c1,the carrier of c1;
assume that
E14: for b1 being Element of Funcs the carrier of c1,the carrier of c1 holds
( b1 in c2 iff ex b2 being Element of c1 st
for b3 being Element of c1 holds b1 . b3 = b3 |^ b2 ) and
E15: for b1 being Element of Funcs the carrier of c1,the carrier of c1 holds
( b1 in c3 iff ex b2 being Element of c1 st
for b3 being Element of c1 holds b1 . b3 = b3 |^ b2 ) ;
E16: c2 c= c3
proof
let c4 be set ; :: according to TARSKI:def 3
assume E17: c4 in c2 ;
then c4 is Function of the carrier of c1,the carrier of c1 by FRAENKEL:def 2;
then reconsider c5 = c4 as Element of Funcs the carrier of c1,the carrier of c1 by FUNCT_2:12;
ex b1 being Element of c1 st
for b2 being Element of c1 holds c5 . b2 = b2 |^ b1 by E14, E17;
hence c4 in c3 by E15;
end;
c3 c= c2
proof
let c4 be set ; :: according to TARSKI:def 3
assume E17: c4 in c3 ;
then c4 is Function of the carrier of c1,the carrier of c1 by FRAENKEL:def 2;
then reconsider c5 = c4 as Element of Funcs the carrier of c1,the carrier of c1 by FUNCT_2:12;
ex b1 being Element of c1 st
for b2 being Element of c1 holds c5 . b2 = b2 |^ b1 by E15, E17;
hence c4 in c2 by E14;
end;
hence c2 = c3 by E16, XBOOLE_0:def 10;
end;
end;

:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
for b1 being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of b1,the carrier of b1 holds
( b2 = InnAut b1 iff for b3 being Element of Funcs the carrier of b1,the carrier of b1 holds
( b3 in b2 iff ex b4 being Element of b1 st
for b5 being Element of b1 holds b3 . b5 = b5 |^ b4 ) );

theorem Th12: :: AUTGROUP:12
for b1 being strict Group holds InnAut b1 c= Funcs the carrier of b1,the carrier of b1
proof
let c1 be strict Group;
let c2 be set ; :: according to TARSKI:def 3
assume c2 in InnAut c1 ;
then consider c3 being Element of InnAut c1 such that
E15: c3 = c2 ;
thus c2 in Funcs the carrier of c1,the carrier of c1 by E15, FUNCT_2:12;
end;

theorem Th13: :: AUTGROUP:13
for b1 being strict Group
for b2 being Element of InnAut b1 holds
b2 is Element of Aut b1
proof
let c1 be strict Group;
let c2 be Element of InnAut c1;
E16: c2 is Element of Funcs the carrier of c1,the carrier of c1 by FUNCT_2:12;
now
let c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E17: for b1 being Element of c1 holds c2 . b1 = b1 |^ c5 by E16, Def4;
thus c2 . (c3 * c4) = (c3 * c4) |^ c5 by E17
.= ((c5 " ) * (c3 * c4)) * c5
.= (((c5 " ) * c3) * c4) * c5 by GROUP_1:def 4
.= ((c5 " ) * c3) * (c4 * c5) by GROUP_1:def 4
.= (((c5 " ) * c3) * (1. c1)) * (c4 * c5) by GROUP_1:def 5
.= (((c5 " ) * c3) * (c5 * (c5 " ))) * (c4 * c5) by GROUP_1:def 6
.= ((((c5 " ) * c3) * c5) * (c5 " )) * (c4 * c5) by GROUP_1:def 4
.= (((((c5 " ) * c3) * c5) * (c5 " )) * c4) * c5 by GROUP_1:def 4
.= ((((c5 " ) * c3) * c5) * ((c5 " ) * c4)) * c5 by GROUP_1:def 4
.= (((c5 " ) * c3) * c5) * (((c5 " ) * c4) * c5) by GROUP_1:def 4
.= (((c5 " ) * c3) * c5) * (c4 |^ c5)
.= (c3 |^ c5) * (c4 |^ c5)
.= (c2 . c3) * (c4 |^ c5) by E17
.= (c2 . c3) * (c2 . c4) by E17 ;
end;
then reconsider c3 = c2 as Homomorphism of c1,c1 by GROUP_6:def 7;
E17: c3 is one-to-one
proof
consider c4 being Element of c1 such that
E18: for b1 being Element of c1 holds c3 . b1 = b1 |^ c4 by E16, Def4;
let c5 be set ; :: according to FUNCT_1:def 8
let c6 be set ;
assume that
E19: c5 in dom c3 and
E20: c6 in dom c3 and
E21: c3 . c5 = c3 . c6 ;
consider c7, c8 being Element of c1 such that
E22: ( c7 = c5 & c8 = c6 ) by E19, E20;
c3 . c7 = c8 |^ c4 by E18, E21, E22;
then c7 |^ c4 = c8 |^ c4 by E18;
then ((c4 " ) * c7) * c4 = c8 |^ c4 ;
then c4 * (((c4 " ) * c7) * c4) = c4 * (((c4 " ) * c8) * c4) ;
then c4 * ((c4 " ) * (c7 * c4)) = c4 * (((c4 " ) * c8) * c4) by GROUP_1:def 4;
then (c4 * (c4 " )) * (c7 * c4) = c4 * (((c4 " ) * c8) * c4) by GROUP_1:def 4;
then (c4 * (c4 " )) * (c7 * c4) = c4 * ((c4 " ) * (c8 * c4)) by GROUP_1:def 4;
then (c4 * (c4 " )) * (c7 * c4) = (c4 * (c4 " )) * (c8 * c4) by GROUP_1:def 4;
then (1. c1) * (c7 * c4) = (c4 * (c4 " )) * (c8 * c4) by GROUP_1:def 6;
then (1. c1) * (c7 * c4) = (1. c1) * (c8 * c4) by GROUP_1:def 6;
then c7 * c4 = (1. c1) * (c8 * c4) by GROUP_1:def 5;
then (c7 * c4) * (c4 " ) = (c8 * c4) * (c4 " ) by GROUP_1:def 5;
then c7 * (c4 * (c4 " )) = (c8 * c4) * (c4 " ) by GROUP_1:def 4;
then c7 * (c4 * (c4 " )) = c8 * (c4 * (c4 " )) by GROUP_1:def 4;
then c7 * (1. c1) = c8 * (c4 * (c4 " )) by GROUP_1:def 6;
then c7 * (1. c1) = c8 * (1. c1) by GROUP_1:def 6;
then c7 = c8 * (1. c1) by GROUP_1:def 5;
hence c<