let A, B be non empty set ; :: thesis: ( A c= B implies A *+^ is SubStr of B *+^ )
H₁(A *+^ ) = A * by Def34;
then A1: dom H₂(A *+^ ) = [:(A * ),(A * ):] by FUNCT_2:def 1;
H₁(B *+^ ) = B * by Def34;
then A2: dom H₂(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:83;

A4: now

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

end;

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