consider j being Nat such that
A1: i = j + 1 by NAT_1:6;
A2: x |^|^ (j + 1) = x |^|^ (Segm (j + 1))
.= x |^|^ (succ (Segm j)) by NAT_1:38
.= exp (x,(x |^|^ j)) by ORDINAL5:14
.= x |^ (x |^|^ j) ;

per cases ( x |^|^ j > 0 or x |^|^ j = 0 ) ;

suppose x |^|^ j > 0 ; :: thesis: x |^|^ i is even

hence x |^|^ i is even by A2, A1; :: thesis: verum

end;

suppose x |^|^ j = 0 ; :: thesis: x |^|^ i is even

hence x |^|^ i is even by Th1; :: thesis: verum

end;

end;