let G be Group; :: thesis: for phi being Automorphism of G holds phi .: (commutators G) = commutators G
let phi be Automorphism of G; :: thesis: phi .: (commutators G) = commutators G
for g being object st g in commutators G holds
g in phi .: (commutators G)

proof

let g be object ; :: thesis: ( g in commutators G implies g in phi .: (commutators G) )
assume B1: g in commutators G ; :: thesis: g in phi .: (commutators G)
then reconsider g = g as Element of G ;
consider a, b being Element of G such that
B2: g = [.a,b.] by B1, GROUP_5:58;
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
set x = psi . a;
set y = psi . b;
set h = [.(psi . a),(psi . b).];
dom phi = the carrier of G by FUNCT_2:def 1;
then B3: ( [.(psi . a),(psi . b).] in dom phi & [.(psi . a),(psi . b).] in commutators G & phi . ((phi ") . g) = g ) by Th4;
psi . g = psi . [.a,b.] by B2
.= [.(psi . a),(psi . b).] by GROUP_6:34
.= [.(psi . a),(psi . b).] ;
hence g in phi .: (commutators G) by B3, FUNCT_1:def 6; :: thesis: verum

end;

then P1: commutators G c= phi .: (commutators G) ;
for h being object st h in phi .: (commutators G) holds
h in commutators G

proof

let h be object ; :: thesis: ( h in phi .: (commutators G) implies h in commutators G )
assume B1: h in phi .: (commutators G) ; :: thesis: h in commutators G
consider g being object such that
g in dom phi and
B2: g in commutators G and
B3: h = phi . g by B1, FUNCT_1:def 6;
consider a, b being Element of G such that
B4: g = [.a,b.] by B2, GROUP_5:58;
h = phi . g by B3
.= phi . [.a,b.] by B4
.= [.(phi . a),(phi . b).] by GROUP_6:34 ;
hence h in commutators G ; :: thesis: verum

end;

then phi .: (commutators G) c= commutators G ;
hence commutators G = phi .: (commutators G) by P1, XBOOLE_0:def 10; :: thesis: verum