let d1, d2 be Element of (GF p); :: thesis: ( ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) implies d1 = d2 )
assume A1: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; :: thesis: ( ex g4, g27 being Element of (GF p) st
( g4 = 4 mod p & g27 = 27 mod p & not d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) or d1 = d2 )
assume A2: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; :: thesis: d1 = d2
reconsider g4 = 4 mod p as Element of (GF p) by Th14;
reconsider g27 = 27 mod p as Element of (GF p) by Th14;
thus d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) by A1
.= d2 by A2 ; :: thesis: verum