set G = Group_of_Perm 2;

A1: now :: thesis:

let H be strict normal Subgroup of Group_of_Perm 2; :: thesis:
assume A2: H <> (Omega). (Group_of_Perm 2) ; :: thesis:
assume A3: H <> (1). (Group_of_Perm 2) ; :: thesis:
1_ (Group_of_Perm 2) in H by GROUP_2:46;
then 1_ (Group_of_Perm 2) in the carrier of H by STRUCT_0:def 5;
then {(1_ (Group_of_Perm 2))} c= the carrier of H by ZFMISC_1:31;
then {<*1,2*>} c= the carrier of H by FINSEQ_2:52, MATRIX_1:15;
then A4: <*1,2*> in the carrier of H by ZFMISC_1:31;
the carrier of H c= the carrier of (Group_of_Perm 2) by GROUP_2:def 5;
then A5: the carrier of H c= {<*1,2*>,<*2,1*>} by MATRIX_1:def 13, MATRIX_7:3;

per cases by A5, ZFMISC_1:36;

suppose the carrier of H = {} ; :: thesis:

hence contradiction ; :: thesis:

end;

suppose the carrier of H = {<*1,2*>} ; :: thesis:

then {(1_ (Group_of_Perm 2))} = the carrier of H by FINSEQ_2:52, MATRIX_1:15;
hence contradiction by A3, GROUP_2:def 7; :: thesis:

end;

suppose the carrier of H = {<*2,1*>} ; :: thesis:

then <*2,1*> . 1 = <*1,2*> . 1 by A4, TARSKI:def 1;
then 2 = <*1,2*> . 1 by FINSEQ_1:44;
hence contradiction by FINSEQ_1:44; :: thesis:

end;

suppose the carrier of H = {<*1,2*>,<*2,1*>} ; :: thesis:

then the carrier of H = the carrier of (Group_of_Perm 2) by MATRIX_1:def 13, MATRIX_7:3;
hence contradiction by A2, GROUP_2:61; :: thesis:

end;

end;

end;

now :: thesis:

assume Group_of_Perm 2 is trivial ; :: thesis:
then consider e being object such that
A6: the carrier of (Group_of_Perm 2) = {e} ;
Permutations 2 = {e} by A6, MATRIX_1:def 13;
then <*2,1*> = <*1,2*> by MATRIX_7:3, ZFMISC_1:5;
then 2 = <*1,2*> . 1 by FINSEQ_1:44;
hence contradiction by FINSEQ_1:44; :: thesis:

end;

hence Group_of_Perm 2 is simple by A1; :: thesis: