set Gp2 = Group_of_Perm 2;
consider G being non empty HGrWOpStr over O such that
A1: ( G is strict & G is distributive & G is Group-like & G is associative ) and
A2: Group_of_Perm 2 = multMagma(# the carrier of G, the multF of G #) by Lm2;
reconsider G = G as strict GroupWithOperators of O by A1;
take G ; :: thesis:

end;

reconsider G9 = G as Group ;
consider H being strict normal StableSubgroup of G such that
A5: H <> (Omega). G and
A6: H <> (1). G by A4;
reconsider H9 = multMagma(# the carrier of H, the multF of H #) as strict normal Subgroup of G by Lm6;
reconsider H9 = H9 as strict normal Subgroup of G9 ;
set H99 = H9;
( the carrier of H9 c= the carrier of G9 & the multF of H9 = the multF of G9 || the carrier of H9 ) by GROUP_2:def 5;
then reconsider H99 = H9 as strict Subgroup of Group_of_Perm 2 by A2, GROUP_2:def 5;

let A be Subset of (Group_of_Perm 2); :: thesis:
reconsider A9 = A as Subset of G9 by A2;
A * H99 = A9 * H9 by A2, Lm7
.= H9 * A9 by GROUP_3:120 ;
hence A * H99 = H99 * A by A2, Lm7; :: thesis:

end;

then reconsider H99 = H99 as strict normal Subgroup of Group_of_Perm 2 by GROUP_3:120;

reconsider e = 1_ (Group_of_Perm 2) as Element of G by A2;

let h be Element of G; :: thesis:
reconsider h9 = h as Element of (Group_of_Perm 2) by A2;
h * e = h9 * (1_ (Group_of_Perm 2)) by A2
.= h9 by GROUP_1:def 4 ;
hence h * e = h ; :: thesis:
e * h = (1_ (Group_of_Perm 2)) * h9 by A2
.= h9 by GROUP_1:def 4 ;
hence e * h = h ; :: thesis:

end;

end;

end;