26 = 13 * 2 ;
then 3 |^ 3,1 are_congruent_mod 13 by Lm1109;
then (3 |^ 3) |^ 368,1 |^ 368 are_congruent_mod 13 by GR_CY_3:34;
then (3 |^ 1104) * (3 |^ 1),1 * 3 are_congruent_mod 13 by Lm1134, INT_4:11;
hence 13 divides (3 |^ 1105) - 3 by Lm1139; :: thesis: verum