let Y, X be set ; :: thesis: ( Y c= X implies GPFuncs Y is SubStr of GPFuncs X )
H1( GPFuncs Y) = PFuncs Y,Y by Def37;
then A1: dom H2( GPFuncs Y) = [:(PFuncs Y,Y),(PFuncs Y,Y):] by FUNCT_2:def 1;
H1( GPFuncs X) = PFuncs X,X by Def37;
then A2: dom H2( GPFuncs X) = [:(PFuncs X,X),(PFuncs X,X):] by FUNCT_2:def 1;
assume Y c= X ; :: thesis: GPFuncs Y is SubStr of GPFuncs X
then A3: PFuncs Y,Y c= PFuncs X,X by PARTFUN1:128;
A4: now
let x be set ; :: thesis: ( x in [:(PFuncs Y,Y),(PFuncs Y,Y):] implies H2( GPFuncs Y) . x = H2( GPFuncs X) . x )
assume A5: x in [:(PFuncs Y,Y),(PFuncs Y,Y):] ; :: thesis: H2( GPFuncs Y) . x = H2( GPFuncs X) . x
then A6: ( x `1 in PFuncs Y,Y & x `2 in PFuncs Y,Y ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Element of (GPFuncs Y) by Def37;
reconsider y1 = x `1 , y2 = x `2 as Element of (GPFuncs X) by A3, A6, Def37;
thus H2( GPFuncs Y) . x = x1 [*] x2 by A5, MCART_1:23
.= x1 (*) x2 by Def37
.= y1 [*] y2 by Def37
.= H2( GPFuncs X) . x by A5, MCART_1:23 ; :: thesis: verum
end;
[:(PFuncs Y,Y),(PFuncs Y,Y):] c= [:(PFuncs X,X),(PFuncs X,X):] by A3, ZFMISC_1:119;
hence H2( GPFuncs Y) c= H2( GPFuncs X) by A1, A2, A4, GRFUNC_1:8; :: according to MONOID_0:def 23 :: thesis: verum