let X be set ; 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 ; for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)
let H be non empty SubStr of G; .: (H,X) is SubStr of .: (G,X)
A1:
H1( .: (H,X)) = (H1(H),H3(H)) .: X
by Th17;
( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X )
by Th17, MONOID_0:def 23;
hence
H1( .: (H,X)) c= H1( .: (G,X))
by A1, Th16; MONOID_0:def 23 verum