let N be multLoopStr ; :: thesis: for M being RelExtension of N holds 1. N = 1. M
let M be RelExtension of N; :: thesis: 1. N = 1. M
multLoopStr(# the carrier of N, the multF of N, the OneF of N #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #) by RE;
hence 1. N = 1. M ; :: thesis: verum