:: deftheorem defines == FIELD_7:def 1 :
for L1, L2 being doubleLoopStr holds
( L1 == L2 iff doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) );