0. L <> 1. L ;
hence not doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is degenerated ; :: thesis: verum