1 in INT.Group 2 by EltsOfINTGroup2;
then reconsider g1 = 1, a2 = 1 as Element of (INT.Group 2) ;
reconsider x = <*g1,(1_ (INT.Group 2))*>, y = <*(1_ (INT.Group 2)),a2*> as Element of (Dihedral_group 2) by Th9;
A1: for k being Nat st k < 2 holds
(x |^ k) * y = y * (x |^ k)

proof

let k be Nat; :: thesis: ( k < 2 implies (x |^ k) * y = y * (x |^ k) )
assume k < 2 ; :: thesis: (x |^ k) * y = y * (x |^ k)
then ( k = 0 or k = 1 ) by NAT_1:23;

per cases then ( k = 0 or k = 1 ) ;

suppose B1: k = 0 ; :: thesis: (x |^ k) * y = y * (x |^ k)

hence (x |^ k) * y = (1_ (Dihedral_group 2)) * y by GROUP_1:25
.= y by GROUP_1:def 4
.= y * (1_ (Dihedral_group 2)) by GROUP_1:def 4
.= y * (x |^ 0) by GROUP_1:25
.= y * (x |^ k) by B1 ;
:: thesis: verum

end;

suppose B2: k = 1 ; :: thesis: (x |^ k) * y = y * (x |^ k)

thus y * (x |^ k) = (x |^ (2 - k)) * y by Th106
.= (x |^ k) * y by B2 ; :: thesis: verum

end;

end;

end;

A2: for k1, k2 being Nat holds (x |^ k1) * (x |^ k2) = (x |^ k2) * (x |^ k1)

proof

let k1, k2 be Nat; :: thesis: (x |^ k1) * (x |^ k2) = (x |^ k2) * (x |^ k1)
thus (x |^ k1) * (x |^ k2) = x |^ (k1 + k2) by GROUP_1:33
.= (x |^ k2) * (x |^ k1) by GROUP_1:33 ; :: thesis: verum

end;

for z1, z2 being Element of (Dihedral_group 2) holds z1 * z2 = z2 * z1

proof

let z1, z2 be Element of (Dihedral_group 2); :: thesis: z1 * z2 = z2 * z1
consider k1 being Nat such that
A3: ( k1 < 2 & ( z1 = (x |^ k1) * y or z1 = x |^ k1 ) ) by Th108;
consider k2 being Nat such that
A4: ( k2 < 2 & ( z2 = (x |^ k2) * y or z2 = x |^ k2 ) ) by Th108;

per cases ( z1 = (x |^ k1) * y or z1 = x |^ k1 ) by A3;

suppose A5: z1 = (x |^ k1) * y ; :: thesis: z1 * z2 = z2 * z1

per cases ( z2 = (x |^ k2) * y or z2 = x |^ k2 ) by A4;

suppose A6: z2 = (x |^ k2) * y ; :: thesis: z1 * z2 = z2 * z1

hence z1 * z2 = ((x |^ k1) * y) * ((x |^ k2) * y) by A5
.= (y * (x |^ k1)) * ((x |^ k2) * y) by A1, A3
.= y * ((x |^ k1) * ((x |^ k2) * y)) by GROUP_1:def 3
.= y * (((x |^ k1) * (x |^ k2)) * y) by GROUP_1:def 3
.= y * (((x |^ k2) * (x |^ k1)) * y) by A2
.= y * ((x |^ k2) * ((x |^ k1) * y)) by GROUP_1:def 3
.= (y * (x |^ k2)) * ((x |^ k1) * y) by GROUP_1:def 3
.= ((x |^ k2) * y) * ((x |^ k1) * y) by A1, A4
.= z2 * z1 by A5, A6 ;
:: thesis: verum

end;

suppose A9: z2 = x |^ k2 ; :: thesis: z1 * z2 = z2 * z1

hence z1 * z2 = ((x |^ k1) * y) * (x |^ k2) by A5
.= (x |^ k1) * (y * (x |^ k2)) by GROUP_1:def 3
.= (x |^ k1) * ((x |^ k2) * y) by A1, A4
.= ((x |^ k1) * (x |^ k2)) * y by GROUP_1:def 3
.= ((x |^ k2) * (x |^ k1)) * y by A2
.= (x |^ k2) * ((x |^ k1) * y) by GROUP_1:def 3
.= z2 * z1 by A5, A9 ;
:: thesis: verum

end;

end;

end;

suppose A10: z1 = x |^ k1 ; :: thesis: z1 * z2 = z2 * z1

per cases ( z2 = (x |^ k2) * y or z2 = x |^ k2 ) by A4;

suppose A11: z2 = (x |^ k2) * y ; :: thesis: z1 * z2 = z2 * z1

hence z1 * z2 = (x |^ k1) * ((x |^ k2) * y) by A10
.= ((x |^ k1) * (x |^ k2)) * y by GROUP_1:def 3
.= ((x |^ k2) * (x |^ k1)) * y by A2
.= (x |^ k2) * ((x |^ k1) * y) by GROUP_1:def 3
.= (x |^ k2) * (y * (x |^ k1)) by A1, A3
.= ((x |^ k2) * y) * (x |^ k1) by GROUP_1:def 3
.= z2 * z1 by A10, A11 ;
:: thesis: verum

end;

suppose A12: z2 = x |^ k2 ; :: thesis: z1 * z2 = z2 * z1

hence z1 * z2 = (x |^ k1) * (x |^ k2) by A10
.= (x |^ k2) * (x |^ k1) by A2
.= z2 * z1 by A10, A12 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence Dihedral_group 2 is commutative ; :: thesis: verum