let p be 5 _or_greater Prime; 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; 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)) #);
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
;
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;
verum
end;
hence
P is
right_complementable
;
verum
end;
hence
addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_complementable
; verum