let A, B be non empty set ; :: thesis: ( A c= B implies A *+^ is SubStr of B *+^ )
H1(A *+^ ) = A * by Def34;
then A1: dom H2(A *+^ ) = [:(A *),(A *):] by FUNCT_2:def 1;
H1(B *+^ ) = B * by Def34;
then A2: dom H2(B *+^ ) = [:(B *),(B *):] by FUNCT_2:def 1;
assume A c= B ; :: thesis: A *+^ is SubStr of B *+^
then A3: A * c= B * by FINSEQ_1:62;
A4: now :: thesis: for x being object st x in [:(A *),(A *):] holds
H2(A *+^ ) . x = H2(B *+^ ) . x
let x be object ; :: thesis: ( x in [:(A *),(A *):] implies H2(A *+^ ) . x = H2(B *+^ ) . x )
assume A5: x in [:(A *),(A *):] ; :: thesis: H2(A *+^ ) . x = H2(B *+^ ) . x
then A6: ( x `1 in A * & x `2 in A * ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Element of (A *+^) by Def34;
reconsider y1 = x `1 , y2 = x `2 as Element of (B *+^) by A3, A6, Def34;
thus H2(A *+^ ) . x = x1 [*] x2 by A5, MCART_1:21
.= x1 ^ x2 by Def34
.= y1 [*] y2 by Def34
.= H2(B *+^ ) . x by A5, MCART_1:21 ; :: thesis: verum
end;
[:(A *),(A *):] c= [:(B *),(B *):] by A3, ZFMISC_1:96;
hence H2(A *+^ ) c= H2(B *+^ ) by A1, A2, A4, GRFUNC_1:2; :: according to MONOID_0:def 23 :: thesis: verum