let G be non empty multMagma ; :: thesis: for M being MonoidalExtension of G holds
( the carrier of M = the carrier of G & the multF of M = the multF of G & ( for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
let M be MonoidalExtension of G; :: thesis: ( the carrier of M = the carrier of G & the multF of M = the multF of G & ( for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
A1: multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence ( H₁(M) = H₁(G) & H₂(M) = H₂(G) ) ; :: thesis: for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a, b be Element of M; :: thesis: for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a9, b9 be Element of G; :: thesis: ( a = a9 & b = b9 implies a * b = a9 * b9 )
thus ( a = a9 & b = b9 implies a * b = a9 * b9 ) by A1; :: thesis: verum