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

for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

let H be non empty SubStr of G; :: thesis: .: (H,X) is SubStr of .: (G,X)

A1: 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;

hence H_{1}( .: (H,X)) c= H_{1}( .: (G,X))
by A1, Th16; :: according to MONOID_0:def 23 :: thesis: verum

for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

let H be non empty SubStr of G; :: thesis: .: (H,X) is SubStr of .: (G,X)

A1: H

( H

hence H