reconsider g40 = 4 mod p as Element of (GF p) by Th14;
reconsider g270 = 27 mod p as Element of (GF p) by Th14;
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)) ; :: thesis: verum