set r = the Relation of the carrier of M;
set R = RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #);
multLoopStr(# the carrier of RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #), the multF of RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #), the OneF of RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #) #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #) ;
then RelMonoid(# the carrier of M, the multF of M, the OneF of M, the Relation of the carrier of M #) is RelExtension of M by RE;
hence ex b₁ being RelExtension of M st b₁ is strict ; :: thesis: verum