let G be non empty unital multMagma ; :: thesis: for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2
let M1, M2 be strict well-unital MonoidalExtension of G; :: thesis: M1 = M2
A1: ( H₃(M1) = the_unity_wrt H₂(M1) & H₃(M2) = the_unity_wrt H₂(M2) ) by Th17;
( multMagma(# the carrier of M1, the multF of M1 #) = multMagma(# the carrier of G, the multF of G #) & multMagma(# the carrier of M2, the multF of M2 #) = multMagma(# the carrier of G, the multF of G #) ) by Def22;
hence M1 = M2 by A1; :: thesis: verum