let p be Prime; :: thesis: for a, b being Element of multMagma(# (Segm0 p),(multint0 p) #)
for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
let a, b be Element of multMagma(# (Segm0 p),(multint0 p) #); :: thesis: for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
let x, y be Element of (INT.Ring p); :: thesis: ( a = x & y = b implies x * y = a * b )
assume that
A1: a = x and
A2: y = b ; :: thesis: x * y = a * b
thus a * b = (multint p) . [a,b] by FUNCT_1:49
.= x * y by A1, A2 ; :: thesis: verum