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