let R be RelExtension of M; :: thesis: not R is empty
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 #) by RE;
hence not R is empty ; :: thesis: verum