let Y, X be set ; :: thesis: ( Y c= X implies GPFuncs Y is SubStr of GPFuncs X )
assume
Y c= X
; :: thesis: GPFuncs Y is SubStr of GPFuncs X
then A1:
PFuncs Y,Y c= PFuncs X,X
by PARTFUN1:128;
then A2:
[:(PFuncs Y,Y),(PFuncs Y,Y):] c= [:(PFuncs X,X),(PFuncs X,X):]
by ZFMISC_1:119;
( H1( GPFuncs Y) = PFuncs Y,Y & H1( GPFuncs X) = PFuncs X,X )
by Def37;
then A3:
( dom H2( GPFuncs Y) = [:(PFuncs Y,Y),(PFuncs Y,Y):] & dom H2( GPFuncs X) = [:(PFuncs X,X),(PFuncs X,X):] )
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in [:(PFuncs Y,Y),(PFuncs Y,Y):] implies H2( GPFuncs Y) . x = H2( GPFuncs X) . x )assume A4:
x in [:(PFuncs Y,Y),(PFuncs Y,Y):]
;
:: thesis: H2( GPFuncs Y) . x = H2( GPFuncs X) . xthen A5:
(
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 A1, A5, Def37;
thus H2(
GPFuncs Y)
. x =
x1 [*] x2
by A4, MCART_1:23
.=
x1 (*) x2
by Def37
.=
y1 [*] y2
by Def37
.=
H2(
GPFuncs X)
. x
by A4, MCART_1:23
;
:: thesis: verum end;
hence
H2( GPFuncs Y) c= H2( GPFuncs X)
by A2, A3, GRFUNC_1:8; :: according to MONOID_0:def 23 :: thesis: verum