let j1 be Integer; :: thesis: j1 = (@' 1) |^ j1
consider k being Nat such that
A1: ( j1 = k or j1 = - k ) by INT_1:2;
per cases ( j1 = k or j1 = - k ) by A1;
suppose j1 = k ; :: thesis: j1 = (@' 1) |^ j1
hence j1 = (@' 1) |^ j1 by Lm4; :: thesis: verum
end;
suppose A2: j1 = - k ; :: thesis: j1 = (@' 1) |^ j1
reconsider k9 = k as Integer ;
reconsider k9 = k9 as Element of INT.Group by INT_1:def 2;
(@' 1) |^ j1 = ((@' 1) |^ k) " by A2, GROUP_1:36
.= k9 " by Lm4
.= j1 by A2, Th15 ;
hence j1 = (@' 1) |^ j1 ; :: thesis: verum
end;
end;