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 a * b = b * a

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: a * b = b * a
reconsider x = a, y = b as Element of L ;
thus a * b = x * y
.= y * x by GROUP_1:def 12
.= b * a ; :: 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 commutative ; :: thesis: verum