let X, Y 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:50;
A4: now :: thesis: for x being object st x in [:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] holds
H2( GPFuncs Y) . x = H2( GPFuncs X) . x
let x be object ; :: 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:21
.= x2 (*) x1 by Def37
.= y1 [*] y2 by Def37
.= H2( GPFuncs X) . x by A5, MCART_1:21 ; :: thesis: verum
end;
[:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] c= [:(PFuncs (X,X)),(PFuncs (X,X)):] by A3, ZFMISC_1:96;
hence H2( GPFuncs Y) c= H2( GPFuncs X) by A1, A2, A4, GRFUNC_1:2; :: according to MONOID_0:def 23 :: thesis: verum