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 H2(N) = [:H1(N),H1(N):] by FUNCT_2:def 1;
A2: dom H2(G) = [:H1(G),H1(G):] by FUNCT_2:def 1;
H2(H) c= H2(G) by Def23;
then A3: dom H2(H) c= dom H2(G) by GRFUNC_1:2;
A4: dom H2(H) = [:H1(H),H1(H):] by FUNCT_2:def 1;
thus H1(H) c= H1(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 H1(H) or x in H1(G) )
assume x in H1(H) ; :: thesis: x in H1(G)
then [x,x] in dom H2(H) by A4, ZFMISC_1:87;
hence x in H1(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 )
H2(N) c= H2(G) by Def24;
then A5: dom H2(N) c= dom H2(G) by GRFUNC_1:2;
assume x in H1(N) ; :: thesis: x in the carrier of G
then [x,x] in dom H2(N) by A1, ZFMISC_1:87;
hence x in the carrier of G by A5, A2, ZFMISC_1:87; :: thesis: verum