let p be Prime; :: thesis: for R being p -characteristic Ring
for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)
let R be p -characteristic Ring; :: thesis: for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)
let i be Integer; :: thesis: i '*' (1. R) = (i mod p) '*' (1. R)
Char R = p by Def6;
then A1: p '*' (1. R) = 0. R by Def5;
A2: ((i div p) * p) '*' (1. R) = ((i div p) '*' (1. R)) * (p '*' (1. R)) by Th66
.= 0. R by A1 ;
thus i '*' (1. R) = (((i div p) * p) + (i mod p)) '*' (1. R) by INT_1:59
.= (0. R) + ((i mod p) '*' (1. R)) by A2, Th61
.= (i mod p) '*' (1. R) ; :: thesis: verum