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, b 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
( not a * b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or a = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) )

let a, b 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: ( not a * b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or a = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) )
reconsider x = a, y = b as Element of L ;
assume a * b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) ; :: thesis: ( a = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) )
then x * y = 0. L ;
hence ( a = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) or b = 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) ) by VECTSP_2:def 1; :: 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 domRing-like by VECTSP_2:def 1; :: thesis: verum