let f1, f2 be Function of [: the carrier of (GF p), the carrier of (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))); :: thesis: ( ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f1 . (a,x) = (i mod p) * x ) & ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f2 . (a,x) = (i mod p) * x ) implies f1 = f2 )

assume A4: for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f1 . (a,x) = (i mod p) * x ; :: thesis: ( ex a being Element of (GF p) ex i being Element of INT.Ring ex x being Element of (VectQuot (V,(p (*) V))) st

( a = i mod p & not f2 . (a,x) = (i mod p) * x ) or f1 = f2 )

assume A5: for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f2 . (a,x) = (i mod p) * x ; :: thesis: f1 = f2

let a, x be set ; :: according to BINOP_1:def 21 :: thesis: ( not a in the carrier of (GF p) or not x in the carrier of (VectQuot (V,(p (*) V))) or f1 . (a,x) = f2 . (a,x) )

assume A6: ( a in the carrier of (GF p) & x in the carrier of (VectQuot (V,(p (*) V))) ) ; :: thesis: f1 . (a,x) = f2 . (a,x)

then reconsider a0 = a as Element of (GF p) ;

reconsider x0 = x as Element of (VectQuot (V,(p (*) V))) by A6;

consider i being Nat such that

A7: a0 = i mod p by EC_PF_1:13;

reconsider i = i as Element of INT.Ring by Lem1;

thus f1 . (a,x) = (i mod p) * x0 by A4, A7

.= f2 . (a,x) by A5, A7 ; :: thesis: verum

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f1 . (a,x) = (i mod p) * x ) & ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f2 . (a,x) = (i mod p) * x ) implies f1 = f2 )

assume A4: for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f1 . (a,x) = (i mod p) * x ; :: thesis: ( ex a being Element of (GF p) ex i being Element of INT.Ring ex x being Element of (VectQuot (V,(p (*) V))) st

( a = i mod p & not f2 . (a,x) = (i mod p) * x ) or f1 = f2 )

assume A5: for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds

f2 . (a,x) = (i mod p) * x ; :: thesis: f1 = f2

let a, x be set ; :: according to BINOP_1:def 21 :: thesis: ( not a in the carrier of (GF p) or not x in the carrier of (VectQuot (V,(p (*) V))) or f1 . (a,x) = f2 . (a,x) )

assume A6: ( a in the carrier of (GF p) & x in the carrier of (VectQuot (V,(p (*) V))) ) ; :: thesis: f1 . (a,x) = f2 . (a,x)

then reconsider a0 = a as Element of (GF p) ;

reconsider x0 = x as Element of (VectQuot (V,(p (*) V))) by A6;

consider i being Nat such that

A7: a0 = i mod p by EC_PF_1:13;

reconsider i = i as Element of INT.Ring by Lem1;

thus f1 . (a,x) = (i mod p) * x0 by A4, A7

.= f2 . (a,x) by A5, A7 ; :: thesis: verum