let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
O is_a_unity_wrt addell_AffCo (z,p)
let z be Element of EC_WParam p; :: thesis: for O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
O is_a_unity_wrt addell_AffCo (z,p)
let O be Element of EC_SetAffCo (z,p); :: thesis: ( O = [0,1,0] implies O is_a_unity_wrt addell_AffCo (z,p) )
assume A1: O = [0,1,0] ; :: thesis: O is_a_unity_wrt addell_AffCo (z,p)
for P being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (O,P) = P by A1, ThLeftZeroedAffCo;
then A2: O is_a_left_unity_wrt addell_AffCo (z,p) by BINOP_1:def 5;
for P being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (P,O) = P by A1, ThRightZeroedAffCo;
hence O is_a_unity_wrt addell_AffCo (z,p) by A2, BINOP_1:def 6, BINOP_1:def 7; :: thesis: verum