let G be Group; :: thesis: for H, K being strict characteristic Subgroup of G
for phi being Automorphism of G holds phi .: (commutators (H,K)) = commutators (H,K)
let H, K be strict characteristic Subgroup of G; :: thesis: for phi being Automorphism of G holds phi .: (commutators (H,K)) = commutators (H,K)
let phi be Automorphism of G; :: thesis: phi .: (commutators (H,K)) = commutators (H,K)
A1: dom phi = the carrier of G by FUNCT_2:def 1;
for x being object st x in commutators (H,K) holds
x in phi .: (commutators (H,K))

proof

let x be object ; :: thesis: ( x in commutators (H,K) implies x in phi .: (commutators (H,K)) )
assume B0: x in commutators (H,K) ; :: thesis: x in phi .: (commutators (H,K))
then reconsider g = x as Element of G ;
consider h, k being Element of G such that
B1: x = [.h,k.] and
B2: ( h in H & k in K ) by B0, GROUP_5:52;
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
set a = psi . h;
set b = psi . k;
B3: ( psi . h in H & psi . k in K ) by B2, Th50;
B4: psi . x = psi . [.h,k.] by B1
.= [.(psi . h),(psi . k).] by GROUP_6:34
.= [.(psi . h),(psi . k).] ;
B5: phi . [.(psi . h),(psi . k).] = phi . (psi . x) by B4
.= g by Th4 ;
[.(psi . h),(psi . k).] in commutators (H,K) by B3;
hence x in phi .: (commutators (H,K)) by B5, A1, FUNCT_1:def 6; :: thesis: verum

end;

then A2: commutators (H,K) c= phi .: (commutators (H,K)) ;
for y being object st y in phi .: (commutators (H,K)) holds
y in commutators (H,K)

proof

let y be object ; :: thesis: ( y in phi .: (commutators (H,K)) implies y in commutators (H,K) )
assume y in phi .: (commutators (H,K)) ; :: thesis: y in commutators (H,K)
then consider x being object such that
B2: ( x in dom phi & x in commutators (H,K) & y = phi . x ) by FUNCT_1:def 6;
consider h, k being Element of G such that
B3: x = [.h,k.] and
B4: ( h in H & k in K ) by B2, GROUP_5:52;
B5: ( phi . h in H & phi . k in K ) by B4, Th50;
phi . x = phi . [.h,k.] by B3
.= [.(phi . h),(phi . k).] by GROUP_6:34 ;
hence y in commutators (H,K) by B2, B5; :: thesis: verum

end;

then phi .: (commutators (H,K)) c= commutators (H,K) ;
hence phi .: (commutators (H,K)) = commutators (H,K) by A2, XBOOLE_0:def 10; :: thesis: verum