let D be non empty set ; :: thesis: for f being Element of HFuncs D
for F being with_the_same_arity FinSequence of HFuncs D holds
( dom (f * <:F:>) c= (arity F) -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
set X = D;
let f be Element of HFuncs D; :: thesis: for F being with_the_same_arity FinSequence of HFuncs D holds
( dom (f * <:F:>) c= (arity F) -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
let F be with_the_same_arity FinSequence of HFuncs D; :: thesis: ( dom (f * <:F:>) c= (arity F) -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
A1: dom (f * <:F:>) c= dom <:F:> by RELAT_1:25;
A2: (arity F) -tuples_on D c= D * by FINSEQ_2:142;
dom <:F:> c= (arity F) -tuples_on D by Th40;
hence dom (f * <:F:>) c= (arity F) -tuples_on D by A1; :: thesis: ( rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
then A3: dom (f * <:F:>) c= D * by A2;
thus rng (f * <:F:>) c= D by RELAT_1:def 19; :: thesis: f * <:F:> in HFuncs D
then f * <:F:> is PartFunc of (D *),D by A3, RELSET_1:4;
then f * <:F:> in PFuncs ((D *),D) by PARTFUN1:45;
hence f * <:F:> in HFuncs D ; :: thesis: verum