:: AUTGROUP semantic presentation

E1: 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 ; :: uses 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 GROUP_2:88;
then ((c3 " ) * c5) * c3 in carr c2 by GROUP_3:20;
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 by GROUP_2:def 13;
end;
end;
hence c2 is normal by GROUP_3:142;
end;

E2: 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, GROUP_2:88;
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 by GROUP_3:20;
then c4 |^ c3 in carr c2 by E7, GROUP_3:59;
hence c4 |^ c3 in c2 by GROUP_2:88;
end;

theorem :: 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 E1, E2;

definition
let c1 be strict Group;
func Aut a1 -> FUNCTION_DOMAIN of the carrier of a1,the carrier of a1 means :E3: :: 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 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 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 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 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 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 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 is_epimorphism ) } as set ;
c3 is functional
proof
let c4 be set ; :: uses 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 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; :: uses 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 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 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 is_epimorphism ) ) ;
hence ( c6 is one-to-one & c6 is is_epimorphism ) ;
end; assume E4: ( c6 is one-to-one & c6 is 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 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 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 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 is_epimorphism ) ) ) ;
E5: c2 c= c3
proof
let c4 be set ; :: uses 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 is_epimorphism ) by E3, E6;
hence c4 in c3 by E4;
end;
c3 c= c2
proof
let c4 be set ; :: uses 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 is_epimorphism ) by E4, E6;
hence c4 in c2 by E3;
end;
hence c2 = c3 by E5, XBOOLE_0:def 10;
end;
end;

:: deftheorem E3 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 is_epimorphism ) ) ) );

theorem :: AUTGROUP:2
canceled;

theorem :: 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 ; :: uses 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 E4: :: 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 is_epimorphism
proof
rng c2 = the carrier of c1 by E5, RELAT_1:71;
hence c2 is is_epimorphism by GROUP_6:def 13;
end;
hence id the carrier of c1 is Element of Aut c1 by E5, E3;
end;

theorem E5: :: AUTGROUP:5
for b1 being strict Group
for b2 being Homomorphism of b1,b1 holds
( b2 in Aut b1 iff b2 is 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 is_epimorphism by E3;
c2 is one-to-one by E6, E3;
then c2 is is_monomorphism by GROUP_6:def 12;
hence c2 is is_isomorphism by E7, GROUP_6:def 14;
end;
hereby
assume c2 is is_isomorphism ;
then E6: ( c2 is is_epimorphism & c2 is 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, E3;
end;
end;

E6: 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 E3;
c3 is is_isomorphism by E5;
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 E7: :: 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 E3;
c3 is is_isomorphism by E5;
hence c2 " is Homomorphism of c1,c1 by GROUP_6:72;
end;

theorem E8: :: 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 E3;
E9: c3 is is_isomorphism by E5;
reconsider c4 = c3 " as Homomorphism of c1,c1 by E7;
c4 is is_isomorphism by E9, GROUP_6:73;
then E10: ( c4 is is_epimorphism & c4 is 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, E3;
end;

theorem E9: :: 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 E3;
( c4 is is_isomorphism & c5 is is_isomorphism ) by E5;
then c4 * c5 is is_isomorphism by GROUP_6:74;
hence c2 * c3 is Element of Aut c1 by E5;
end;

definition
let c1 be strict Group;
func AutComp a1 -> BinOp of Aut a1 means :E10: :: 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 E3;
reconsider c6 = c4 * c5 as Element of Aut c1 by E9;
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 1(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 E10 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 a1 -> 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: now
let c3, c4 be Element of (HGrStr (Aut c1),(AutComp c1));
let c5, c6 be Element of Aut c1;
assume ( c3 = c5 & c4 = c6 ) ;
hence c3 * c4 = (AutComp c1) . c5,c6
.= c5 * c6 by E10 ;

end;
thus for b1, b2, b3 being Element of (HGrStr (Aut c1),(AutComp c1)) holds (b1 * b2) * b3 = b1 * (b2 * b3) :: uses 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 ) ) :: uses GROUP_1:def 3
proof
reconsider c3 = id the carrier of c1 as Element of (HGrStr (Aut c1),(AutComp c1)) by E4;
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:74 ;
hence c4 * c3 = c4 by E12;
c3 * c4 = (id the carrier of c1) * c5 by E11, E12
.= c5 by FUNCT_2:74 ;
hence c3 * c4 = c4 by E12;
reconsider c6 = c5 " as Element of (HGrStr (Aut c1),(AutComp c1)) by E8;
take c6 ;
reconsider c7 = c5 as Homomorphism of c1,c1 by E3;
E13: ( c7 is one-to-one & c7 is is_epimorphism ) by E3;
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 defines AutGroup AUTGROUP:def 3 :
for b1 being strict Group holds AutGroup b1 = HGrStr (Aut b1),(AutComp b1);

theorem E11: :: 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 ) )
proof
let c1 be strict Group;
let c2, c3 be Element of (AutGroup c1);
let c4, c5 be Element of Aut c1;
assume E12: ( c2 = c4 & c3 = c5 ) ;
AutGroup c1 = HGrStr (Aut c1),(AutComp c1) ;
hence c2 * c3 = (AutComp c1) . c4,c5 by E12
.= c4 * c5 by E10 ;

end;

theorem E12: :: AUTGROUP:10
for b1 being strict Group holds id the carrier of b1 = 1. (AutGroup b1)
proof
let c1 be strict Group;
AutGroup c1 = HGrStr (Aut c1),(AutComp c1) ;
then reconsider c2 = id the carrier of c1 as Element of (AutGroup c1) by E4;
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 E3;
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:74;
( ( c5 = c4 & c3 = c2 ) implies ( c5 * c3 = c4 * c2 ) ) by E11;
hence id the carrier of c1 = 1. (AutGroup c1) by E13, E14, E15, GROUP_1:15;
end;

theorem E13: :: 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 ;
AutGroup c1 = HGrStr (Aut c1),(AutComp c1) ;
then consider c4 being Element of Aut c1 such that
E15: c4 = c3 " ;
E16: rng c2 = dom c2 by E6
.= the carrier of c1 by E6 ;
c2 is Homomorphism of c1,c1 by E3;
then E17: c2 is one-to-one by E3;
c4 * c2 = (c3 " ) * c3 by E14, E15, E11;
then c4 * c2 = 1. (AutGroup c1) by GROUP_1:def 6;
then c4 * c2 = id the carrier of c1 by E12;
hence c2 " = c3 " by E15, E16, E17, FUNCT_2:36;
end;

definition
let c1 be strict Group;
func InnAut a1 -> FUNCTION_DOMAIN of the carrier of a1,the carrier of a1 means :E14: :: 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 by GROUP_3:def 2 ;
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 ; :: uses 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; :: uses 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 ; :: uses 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 ; :: uses 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 E14 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 :: 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 ; :: uses 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 E15: :: 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, E14;
thus c2 . (c3 * c4) = (c3 * c4) |^ c5 by E17
.= ((c5 " ) * (c3 * c4)) * c5 by GROUP_3:def 2
.= (((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) by GROUP_3:def 2
.= (c3 |^ c5) * (c4 |^ c5) by GROUP_3:def 2
.= (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, E14;
let c5 be set ; :: uses 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 ;
ex b1 being Function st
( c3 = b1 & dom b1 = the carrier of c1 & rng b1 c= the carrier of c1 ) by E16, FUNCT_2:def 2;
then 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 by GROUP_3:def 2;
then c4 * (((c4 " ) * c7) * c4) = c4 * (((c4 " ) * c8) * c4) by GROUP_3:def 2;
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 c5 = c6 by E22, GROUP_1:def 5;
end;
c3 is is_epimorphism
proof
for b1 being set holds
not ( b1 in the carrier of c1 & for b2 being set holds
not ( b2 in dom c3 & b1 = c3 . b2 ) )
proof
consider c4 being Element of c1 such that
E18: for b1 being Element of c1 holds c3 . b1 = b1 |^ c4 by E16, E14;
let c5 be set ;
assume c5 in the carrier of c1 ;
then consider c6 being Element of c1 such that
E19: c6 = c5 ;
take c7 = (c4 * c6) * (c4 " );
ex b1 being Function st
( c3 = b1 & dom b1 = the carrier of c1 & rng b1 c= the carrier of c1 ) by E16, FUNCT_2:def 2;
hence c7 in dom c3 ;
c6 = (1. c1) * c6 by GROUP_1:def 5
.= ((1. c1) * c6) * (1. c1) by GROUP_1:def 5
.= (((c4 " ) * c4) * c6) * (1. c1) by GROUP_1:def 6
.= (((c4 " ) * c4) * c6) * ((c4 " ) * c4) by GROUP_1:def 6
.= ((((c4 " ) * c4) * c6) * (c4 " )) * c4 by GROUP_1:def 4
.= (((c4 " ) * c4) * (c6 * (c4 " ))) * c4 by GROUP_1:def 4
.= ((c4 " ) * (c4 * (c6 * (c4 " )))) * c4 by GROUP_1:def 4
.= ((c4 " ) * c7) * c4 by GROUP_1:def 4
.= c7 |^ c4 by GROUP_3:def 2
.= c3 . c7 by E18 ;
hence c5 = c3 . c7 by E19;
end;
then the carrier of c1 c= rng c3 by FUNCT_1:19;
hence rng c3 = the carrier of c1 by XBOOLE_0:def 10; :: uses GROUP_6:def 13
end;
hence c2 is Element of Aut c1 by E17, E3;
end;

theorem E16: :: AUTGROUP:14
for b1 being strict Group holds InnAut b1 c= Aut b1
proof
let c1 be strict Group;
now
let c2 be set ;
assume c2 in InnAut c1 ;
then consider c3 being Element of InnAut c1 such that
E17: c3 = c2 ;
c3 is Element of Aut c1 by E15;
hence c2 in Aut c1 by E17;
end;
hence InnAut c1 c=