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

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