set G = doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #);

now :: thesis: for a being Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) holds a is right_complementable

let a be Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #); :: thesis: a is right_complementable
reconsider x = a as Element of L ;
consider y being Element of L such that
E1: x + y = 0. L by ALGSTR_0:def 11;
reconsider b = y as Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) ;
a + b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) by E1;
hence a is right_complementable ; :: thesis: verum

end;

hence doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is right_complementable ; :: thesis: verum