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