let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y
let g1 be Element of (INT.Group n); :: thesis: for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y
let a2 be Element of (INT.Group 2); :: thesis: ( a2 = 1 implies for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y )
assume A1: a2 = 1 ; :: thesis: for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y
let x, y be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> implies for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y )
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y )
assume A3: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y
defpred S₁[ Nat] means y * (x |^ $1) = (x |^ (n - $1)) * y;
A4: S₁[ 0 ]

proof

thus y * (x |^ 0) = y * (1_ (Dihedral_group n)) by GROUP_1:25
.= y by GROUP_1:def 4
.= (1_ (Dihedral_group n)) * y by GROUP_1:def 4
.= (x |^ n) * y by A2, Th101
.= (x |^ (n - 0)) * y ; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
y * (x |^ (k + 1)) = y * ((x |^ k) * x) by GROUP_1:34
.= (y * (x |^ k)) * x by GROUP_1:def 3
.= ((x |^ (n - k)) * y) * x by B1
.= (x |^ (n - k)) * (y * x) by GROUP_1:def 3
.= (x |^ (n - k)) * ((x |^ (- 1)) * y) by A1, A2, A3, Th105
.= ((x |^ (n - k)) * (x |^ (- 1))) * y by GROUP_1:def 3
.= (x |^ ((n - k) + (- 1))) * y by GROUP_1:33
.= (x |^ (n - (k + 1))) * y ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
hence for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y ; :: thesis: verum