let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p holds 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) = 0_EC (z,p)
let z be Element of EC_WParam p; :: thesis: 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) = 0_EC (z,p)
set F = multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #);
reconsider E = 0_EC (z,p) as Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ;
for h being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds
( h * E = h & E * h = h )
proof
let h be Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #); :: thesis: ( h * E = h & E * h = h )
reconsider h1 = h as Element of EC_SetAffCo (z,p) ;
X1: 0_EC (z,p) is_a_unity_wrt addell_AffCo (z,p) by ThUnityAffCo;
hence h * E = h by BINOP_1:def 6, BINOP_1:def 7; :: thesis: E * h = h
thus E * h = h by X1, BINOP_1:def 5, BINOP_1:def 7; :: thesis: verum
end;
hence 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) = 0_EC (z,p) by GROUP_1:def 4; :: thesis: verum