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₃(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₁(H9) = the_unity_wrt H₁(G9) by A1, MONOID_0:30;
A3: H₁( .: (H,X)) = (H₁(H),H₃(H)) .: X by Th17;
( H₁(H) c= H₁(G) & H₁( .: (G,X)) = (H₁(G),H₃(G)) .: X ) by Th17, MONOID_0:def 23;
then A4: H₁( .: (H,X)) c= H₁( .: (G,X)) by A3, Th16;
( 1. (.: (G9,X)) = X --> (the_unity_wrt H₁(G)) & 1. (.: (H9,X)) = X --> (the_unity_wrt H₁(H)) ) by Th22;
hence .: (H,X) is MonoidalSubStr of .: (G,X) by A2, A4, MONOID_0:def 25; :: thesis: verum