let X be set ; :: thesis: for G being non empty unital multMagma

for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds

.: (H,X) is MonoidalSubStr of .: (G,X)

let G be non empty unital multMagma ; :: thesis: for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds

.: (H,X) is MonoidalSubStr of .: (G,X)

let H be non empty SubStr of G; :: thesis: ( the_unity_wrt the multF of G in the carrier of H implies .: (H,X) is MonoidalSubStr of .: (G,X) )

assume A1: the_unity_wrt the multF of G in H_{3}(H)
; :: thesis: .: (H,X) is MonoidalSubStr of .: (G,X)

then reconsider G9 = G, H9 = H as non empty unital multMagma by MONOID_0:30;

A2: the_unity_wrt H_{1}(H9) = the_unity_wrt H_{1}(G9)
by A1, MONOID_0:30;

A3: H_{1}( .: (H,X)) = (H_{1}(H),H_{3}(H)) .: X
by Th17;

( H_{1}(H) c= H_{1}(G) & H_{1}( .: (G,X)) = (H_{1}(G),H_{3}(G)) .: X )
by Th17, MONOID_0:def 23;

then A4: H_{1}( .: (H,X)) c= H_{1}( .: (G,X))
by A3, Th16;

( 1. (.: (G9,X)) = X --> (the_unity_wrt H_{1}(G)) & 1. (.: (H9,X)) = X --> (the_unity_wrt H_{1}(H)) )
by Th22;

hence .: (H,X) is MonoidalSubStr of .: (G,X) by A2, A4, MONOID_0:def 25; :: thesis: verum

for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds

.: (H,X) is MonoidalSubStr of .: (G,X)

let G be non empty unital multMagma ; :: thesis: for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds

.: (H,X) is MonoidalSubStr of .: (G,X)

let H be non empty SubStr of G; :: thesis: ( the_unity_wrt the multF of G in the carrier of H implies .: (H,X) is MonoidalSubStr of .: (G,X) )

assume A1: the_unity_wrt the multF of G in H

then reconsider G9 = G, H9 = H as non empty unital multMagma by MONOID_0:30;

A2: the_unity_wrt H

A3: H

( H

then A4: H

( 1. (.: (G9,X)) = X --> (the_unity_wrt H

hence .: (H,X) is MonoidalSubStr of .: (G,X) by A2, A4, MONOID_0:def 25; :: thesis: verum