let G be Group; :: thesis: for H, K being strict characteristic Subgroup of G holds H "\/" K is characteristic Subgroup of G
let H, K be strict characteristic Subgroup of G; :: thesis: H "\/" K is characteristic Subgroup of G
for phi being Automorphism of G
for g being Element of G st g in H "\/" K holds
phi . g in H "\/" K

proof

let phi be Automorphism of G; :: thesis: for g being Element of G st g in H "\/" K holds
phi . g in H "\/" K
let g be Element of G; :: thesis: ( g in H "\/" K implies phi . g in H "\/" K )
assume g in H "\/" K ; :: thesis: phi . g in H "\/" K
then g in H * K by GROUP_4:53;
then consider h, k being Element of G such that
B1: g = h * k and
B2: h in carr H and
B3: k in carr K ;
h in H by B2;
then B4: phi . h in H by Th50;
k in K by B3;
then phi . k in K by Th50;
then (phi . h) * (phi . k) in (carr H) * (carr K) by B4;
then phi . g in H * K by B1, GROUP_6:def 6;
hence phi . g in H "\/" K by GROUP_4:53; :: thesis: verum

end;

hence H "\/" K is characteristic Subgroup of G by Th50; :: thesis: verum