let p be Prime; :: thesis: for x, y being Element of (Z/Z* p)
for i, j being Integer st x = i & y = j holds
x * y = (i * j) mod p
let x, y be Element of (Z/Z* p); :: thesis: for i, j being Integer st x = i & y = j holds
x * y = (i * j) mod p
let i, j be Integer; :: thesis: ( x = i & y = j implies x * y = (i * j) mod p )
assume A1: ( x = i & y = j ) ; :: thesis: x * y = (i * j) mod p
A2: INT.Ring p = doubleLoopStr(# (Segm p),(addint p),(multint p),(In (1,(Segm p))),(In (0,(Segm p))) #) by INT_3:def 12;
A3: Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #) by INT_7:def 4;
then x in Segm0 p ;
then x in (Segm p) \ {0} by INT_2:def 4, INT_7:def 2;
then reconsider xx = x as Element of Segm p by XBOOLE_0:def 5;
y in Segm0 p by A3;
then y in (Segm p) \ {0} by INT_2:def 4, INT_7:def 2;
then reconsider yy = y as Element of Segm p by XBOOLE_0:def 5;
reconsider x1 = xx, y1 = yy as Element of (INT.Ring p) by A2;
A4: x * y = x1 * y1 by INT_7:20;
x1 * y1 = (multint p) . (xx,yy) by A2, ALGSTR_0:def 18;
hence x * y = (i * j) mod p by A4, A1, INT_3:def 10; :: thesis: verum