let G be Group; :: thesis: for A being non empty Subset of G st ( for phi being Automorphism of G holds phi .: A = A ) holds
gr A is characteristic
let A be non empty Subset of G; :: thesis: ( ( for phi being Automorphism of G holds phi .: A = A ) implies gr A is characteristic )
assume A1: for phi being Automorphism of G holds phi .: A = A ; :: thesis: gr A is characteristic
A2: for phi being Automorphism of G
for a being Element of A holds phi . a in A

proof

let phi be Automorphism of G; :: thesis: for a being Element of A holds phi . a in A
let a be Element of A; :: thesis: phi . a in A
dom phi = the carrier of G by FUNCT_2:def 1;
then phi . a in phi .: A by FUNCT_1:def 6;
hence phi . a in A by A1; :: thesis: verum

end;

set H = gr A;
for phi being Automorphism of G holds Image (phi | (gr A)) is Subgroup of gr A

proof

let phi be Automorphism of G; :: thesis: Image (phi | (gr A)) is Subgroup of gr A
B2: for h being Element of G st h in gr A holds
phi . h in gr A

proof

let h be Element of G; :: thesis: ( h in gr A implies phi . h in gr A )
assume h in gr A ; :: thesis: phi . h in gr A
then consider F1 being FinSequence of the carrier of G, I being FinSequence of INT such that
C2: len F1 = len I and
C3: rng F1 c= A and
C4: Product (F1 |^ I) = h by GROUP_4:28;
deffunc H₁( Nat) -> Element of the carrier of G = phi . (F1 /. $1);
consider F2 being FinSequence such that
C5: len F2 = len F1 and
C6: for k being Nat st k in dom F2 holds
F2 . k = H₁(k) from FINSEQ_1:sch 2();
C7: dom F2 = dom F1 by C5, FINSEQ_3:29;
C8: ( F2 is FinSequence of the carrier of G & rng F2 c= A )

proof

D1: for y being object st y in rng F2 holds
y in A

proof

let y be object ; :: thesis: ( y in rng F2 implies y in A )
assume y in rng F2 ; :: thesis: y in A
then consider k being object such that
E2: k in dom F2 and
E3: y = F2 . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by E2;
set x = F1 . k;
F1 . k in rng F1 by FUNCT_1:def 3, E2, C7;
then reconsider x = F1 . k as Element of A by C3;
E4: x = F1 /. k by E2, C7, PARTFUN1:def 6;
y = H₁(k) by E2, E3, C6
.= phi . (F1 /. k) ;
hence y in A by A2, E4; :: thesis: verum

end;

for y being object st y in rng F2 holds
y in the carrier of G

proof

let y be object ; :: thesis: ( y in rng F2 implies y in the carrier of G )
assume y in rng F2 ; :: thesis: y in the carrier of G
then y in A by D1;
hence y in the carrier of G ; :: thesis: verum

end;

hence rng F2 c= the carrier of G ; :: according to FINSEQ_1:def 4 :: thesis: rng F2 c= A
thus rng F2 c= A by D1; :: thesis: verum

end;

then reconsider F2 = F2 as FinSequence of the carrier of G ;
set h2 = Product (F2 |^ I);
( ( for k being Nat st k in dom F1 holds
F2 . k = phi . (F1 . k) ) & len F1 = len I & len F2 = len I )

proof

thus for k being Nat st k in dom F1 holds
F2 . k = phi . (F1 . k) :: thesis: ( len F1 = len I & len F2 = len I )

proof

let k be Nat; :: thesis: ( k in dom F1 implies F2 . k = phi . (F1 . k) )
assume D1: k in dom F1 ; :: thesis: F2 . k = phi . (F1 . k)
then k in dom F2 by C5, FINSEQ_3:29;
then F2 . k = H₁(k) by C6
.= phi . (F1 /. k) ;
hence F2 . k = phi . (F1 . k) by D1, PARTFUN1:def 6; :: thesis: verum

end;

thus len F1 = len I by C2; :: thesis: len F2 = len I
thus len F2 = len I by C2, C5; :: thesis: verum

end;

then ( len F2 = len I & rng F2 c= A & Product (F2 |^ I) = phi . h ) by C4, C8, GROUP_9:125;
hence phi . h in gr A by GROUP_4:28; :: thesis: verum

end;

for h being Element of (gr A) holds phi . h in gr A

proof

let h be Element of (gr A); :: thesis: phi . h in gr A
C1: h in gr A ;
h is Element of G by GROUP_2:42;
hence phi . h in gr A by B2, C1; :: thesis: verum

end;

hence Image (phi | (gr A)) is Subgroup of gr A by Th44; :: thesis: verum

end;

hence gr A is characteristic by Th40; :: thesis: verum