set r = the Relation of the carrier of M;
take R = RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #); :: thesis: multLoopStr(# the carrier of R, the multF of R, the OneF of R #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #)
thus multLoopStr(# the carrier of R, the multF of R, the OneF of R #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #) ; :: thesis: verum