set ECSTR = addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #);
for P being Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) holds (0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #)) + P = P by ThLeftZeroedAffCo;
hence ( addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is left_zeroed & addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_zeroed ) by ALGSTR_1:def 2, ThRightZeroedAffCo; :: thesis: verum