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 a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b' ) )
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 a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b' ) )
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 a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
let a, b be Element of M; :: thesis: for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
let a', b' be Element of G; :: thesis: ( a = a' & b = b' implies a * b = a' * b' )
thus ( a = a' & b = b' implies a * b = a' * b' ) by A1; :: thesis: verum