consider g40 being Element of (GF p) such that
P0: g40 = 4 mod p by GF2;
consider g270 being Element of (GF p) such that
P1: g270 = 27 mod p by GF2;
reconsider d = (g40 * (a |^ 3)) + (g270 * (b |^ 2)) as Element of (GF p) ;
take d ; :: thesis: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d = (g4 * (a |^ 3)) + (g27 * (b |^ 2))
thus for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) by P0, P1; :: thesis: verum