let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G holds the multF of H = the multF of G || the carrier of H
let H be non empty SubStr of G; :: thesis: the multF of H = the multF of G || the carrier of H
( H₂(H) c= H₂(G) & dom H₂(H) = [:H₁(H),H₁(H):] ) by Def23, FUNCT_2:def 1;
hence the multF of H = the multF of G || the carrier of H by GRFUNC_1:23; :: thesis: verum