let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p holds addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_complementable
let z be Element of EC_WParam p; :: thesis: addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_complementable
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 P is right_complementable

proof

let P be Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #); :: thesis: P is right_complementable
ex Q being Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) st P + Q = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #)

proof

set O = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #);
set Q = (compell_AffCo (z,p)) . P;
reconsider Q = (compell_AffCo (z,p)) . P as Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) by FUNCT_2:5;
take Q ; :: thesis: P + Q = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #)
thus P + Q = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) by ThAddCompAffCo; :: thesis: verum

end;

hence P is right_complementable ; :: thesis: verum

end;

hence addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_complementable ; :: thesis: verum