defpred S_{1}[ 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 S_{1}[a,x,z]

A3: for a being Element of (GF p)

for x being Element of (VectQuot (V,(p (*) V))) holds S_{1}[a,x,f . (a,x)]
from BINOP_1:sch 3(A1);

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

$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 S

proof

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
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 S_{1}[a,x,z]

let x be Element of (VectQuot (V,(p (*) V))); :: thesis: ex z being Element of (VectQuot (V,(p (*) V))) st S_{1}[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))) ;

S_{1}[a,x,z]
by A2;

hence ex z being Element of (VectQuot (V,(p (*) V))) st S_{1}[a,x,z]
; :: thesis: verum

end;let x be Element of (VectQuot (V,(p (*) V))); :: thesis: ex z being Element of (VectQuot (V,(p (*) V))) st S

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))) ;

S

hence ex z being Element of (VectQuot (V,(p (*) V))) st S

A3: for a being Element of (GF p)

for x being Element of (VectQuot (V,(p (*) V))) holds S

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