let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a, b being Element of R
for x, y being Element of (R |^ p) st a = x & b = y holds
a * b = x * y
let F be commutative p -characteristic Ring; :: thesis: for a, b being Element of F
for x, y being Element of (F |^ p) st a = x & b = y holds
a * b = x * y
let a, b be Element of F; :: thesis: for x, y being Element of (F |^ p) st a = x & b = y holds
a * b = x * y
let x, y be Element of (F |^ p); :: thesis: ( a = x & b = y implies a * b = x * y )
assume A1: ( a = x & b = y ) ; :: thesis: a * b = x * y
set M = { (a |^ p) where a is Element of F : verum } ;
A2: the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by deffp;
then A3: ( [x,y] in [: { (a |^ p) where a is Element of F : verum } , { (a |^ p) where a is Element of F : verum } :] & [a,b] in [: { (a |^ p) where a is Element of F : verum } , { (a |^ p) where a is Element of F : verum } :] ) by A1, ZFMISC_1:def 2;
thus x * y = ( the multF of F || the carrier of (F |^ p)) . (x,y) by deffp
.= a * b by A1, A2, A3, FUNCT_1:49 ; :: thesis: verum