let M be non empty multLoopStr ; :: thesis: for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 = the carrier of H2 holds
multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
let H1, H2 be non empty MonoidalSubStr of M; :: thesis: ( the carrier of H1 = the carrier of H2 implies multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #) )
assume A1: the carrier of H1 = the carrier of H2 ; :: thesis: multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
reconsider N1 = H1, N2 = H2 as SubStr of M by Th21;
A2: ( H₃(H1) = H₃(M) & H₃(H2) = H₃(M) ) by Def25;
multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) by A1, Th26;
hence multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #) by A2; :: thesis: verum