defpred S1[ Element of (GF p), Element of (VectQuot (V,(p (*) V))), Element of (VectQuot (V,(p (*) V)))] means for i being Element of INT.Ring st \$1 = i mod p holds
\$3 = (i mod p) * \$2;
A1: for a being Element of (GF p)
for x being Element of (VectQuot (V,(p (*) V))) ex z being Element of (VectQuot (V,(p (*) V))) st S1[a,x,z]
proof
let a be Element of (GF p); :: thesis: for x being Element of (VectQuot (V,(p (*) V))) ex z being Element of (VectQuot (V,(p (*) V))) st S1[a,x,z]
let x be Element of (VectQuot (V,(p (*) V))); :: thesis: ex z being Element of (VectQuot (V,(p (*) V))) st S1[a,x,z]
consider i being Nat such that
A2: a = i mod p by EC_PF_1:13;
i in INT by INT_1:def 2;
then reconsider i = i as Element of INT.Ring ;
reconsider z = (i mod p) * x as Element of (VectQuot (V,(p (*) V))) ;
S1[a,x,z] by A2;
hence ex z being Element of (VectQuot (V,(p (*) V))) st S1[a,x,z] ; :: thesis: verum
end;
consider f being Function of [: the carrier of (GF p), the carrier of (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) such that
A3: for a being Element of (GF p)
for x being Element of (VectQuot (V,(p (*) V))) holds S1[a,x,f . (a,x)] from take f ; :: 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
f . (a,x) = (i mod p) * x

thus 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
f . (a,x) = (i mod p) * x by A3; :: thesis: verum