let t be Integer; :: thesis: for n being odd Nat holds (t |^ n) mod 3 = t mod 3
let n be odd Nat; :: thesis: (t |^ n) mod 3 = t mod 3

per cases ( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 ) by Lm3;

suppose A1: t mod 3 = 0 ; :: thesis: (t |^ n) mod 3 = t mod 3

then 0 = ((t mod 3) |^ n) mod 3 ;
hence (t |^ n) mod 3 = t mod 3 by A1, GR_CY_3:30; :: thesis: verum

end;

suppose A1: t mod 3 = 1 ; :: thesis: (t |^ n) mod 3 = t mod 3

then 1 = ((t mod 3) |^ n) mod 3 ;
hence (t |^ n) mod 3 = t mod 3 by A1, GR_CY_3:30; :: thesis: verum

end;

suppose A1: t mod 3 = 2 ; :: thesis: (t |^ n) mod 3 = t mod 3

then 2 = ((t mod 3) |^ n) mod 3 by LmMod;
hence (t |^ n) mod 3 = t mod 3 by A1, GR_CY_3:30; :: thesis: verum

end;

end;