let A, B be non empty set ; :: thesis: ( A c= B implies A *+^ is SubStr of B *+^ )
assume A c= B ; :: thesis: A *+^ is SubStr of B *+^
then A1: A * c= B * by FINSEQ_1:83;
then A2: [:(A * ),(A * ):] c= [:(B * ),(B * ):] by ZFMISC_1:119;
( H₁(A *+^ ) = A * & H₁(B *+^ ) = B * ) by Def34;
then A3: ( dom H₂(A *+^ ) = [:(A * ),(A * ):] & dom H₂(B *+^ ) = [:(B * ),(B * ):] ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in [:(A * ),(A * ):] implies H₂(A *+^ ) . x = H₂(B *+^ ) . x )
assume A4: x in [:(A * ),(A * ):] ; :: thesis: H₂(A *+^ ) . x = H₂(B *+^ ) . x
then A5: ( 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 A1, A5, Def34;
thus H₂(A *+^ ) . x = x1 [*] x2 by A4, MCART_1:23
.= x1 ^ x2 by Def34
.= y1 [*] y2 by Def34
.= H₂(B *+^ ) . x by A4, MCART_1:23 ; :: thesis: verum

end;

hence H₂(A *+^ ) c= H₂(B *+^ ) by A2, A3, GRFUNC_1:8; :: according to MONOID_0:def 23 :: thesis: verum