let p be Prime; :: thesis: for a, b being Element of
for x, y being Element of st a = x & y = b holds
x * y = a * b
let a, b be Element of ; :: thesis: for x, y being Element of st a = x & y = b holds
x * y = a * b
let x, y be Element of ; :: 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:72
.= x * y by A1, A2 ; :: thesis: verum