let a be object ; :: thesis: for N being multLoopStr
for M being RelExtension of N holds
( a is Element of M iff a is Element of N )
let N be multLoopStr ; :: thesis: for M being RelExtension of N holds
( a is Element of M iff a is Element of N )
let M be RelExtension of N; :: thesis: ( a is Element of M iff a is Element of N )
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 ( a is Element of M iff a is Element of N ) ; :: thesis: verum