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 left_complementable
let z be Element of EC_WParam p; :: thesis: addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is left_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 left_complementable

proof

let P be Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #); :: thesis: P is left_complementable
ex Q being Element of addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) st Q + P = 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;
A2: Q + P = (addell_AffCo (z,p)) . (P,Q) by ThCommutativeAffCo
.= 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) by ThAddCompAffCo ;
take Q ; :: thesis: Q + P = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #)
thus Q + P = 0. addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) by A2; :: thesis: verum

end;

hence P is left_complementable ; :: thesis: verum

end;

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