defpred S₁[ Element of (GF p), Element of (Z_ModuleQuot (V,(p (*) V))), Element of (Z_ModuleQuot (V,(p (*) V)))] means for i being Integer st $1 = i mod p holds
$3 = (i mod p) * $2;
A1: for a being Element of (GF p)
for x being Element of (Z_ModuleQuot (V,(p (*) V))) ex z being Element of (Z_ModuleQuot (V,(p (*) V))) st S₁[a,x,z]

proof

let a be Element of (GF p); :: thesis: for x being Element of (Z_ModuleQuot (V,(p (*) V))) ex z being Element of (Z_ModuleQuot (V,(p (*) V))) st S₁[a,x,z]
let x be Element of (Z_ModuleQuot (V,(p (*) V))); :: thesis: ex z being Element of (Z_ModuleQuot (V,(p (*) V))) st S₁[a,x,z]
consider i being Nat such that
A2: a = i mod p by EC_PF_1:13;
reconsider i = i as Integer ;
reconsider z = (i mod p) * x as Element of (Z_ModuleQuot (V,(p (*) V))) ;
S₁[a,x,z] by A2;
hence ex z being Element of (Z_ModuleQuot (V,(p (*) V))) st S₁[a,x,z] ; :: thesis: verum

end;

consider f being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) such that
A3: for a being Element of (GF p)
for x being Element of (Z_ModuleQuot (V,(p (*) V))) holds S₁[a,x,f . (a,x)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for a being Element of (GF p)
for i being Integer
for x being Element of (Z_ModuleQuot (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 Integer
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
f . (a,x) = (i mod p) * x by A3; :: thesis: verum