let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G
for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
let H be non empty SubStr of G; :: thesis: for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
let N be non empty MonoidalSubStr of G; :: thesis: ( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
A1: dom H₂(N) = [:H₁(N),H₁(N):] by FUNCT_2:def 1;
A2: dom H₂(G) = [:H₁(G),H₁(G):] by FUNCT_2:def 1;
H₂(H) c= H₂(G) by Def23;
then A3: dom H₂(H) c= dom H₂(G) by GRFUNC_1:2;
A4: dom H₂(H) = [:H₁(H),H₁(H):] by FUNCT_2:def 1;
thus H₁(H) c= H₁(G) :: thesis: the carrier of N c= the carrier of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(H) or x in H₁(G) )
assume x in H₁(H) ; :: thesis: x in H₁(G)
then [x,x] in dom H₂(H) by A4, ZFMISC_1:87;
hence x in H₁(G) by A3, A2, ZFMISC_1:87; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of N or x in the carrier of G )
H₂(N) c= H₂(G) by Def24;
then A5: dom H₂(N) c= dom H₂(G) by GRFUNC_1:2;
assume x in H₁(N) ; :: thesis: x in the carrier of G
then [x,x] in dom H₂(N) by A1, ZFMISC_1:87;
hence x in the carrier of G by A5, A2, ZFMISC_1:87; :: thesis: verum