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 )
( dom (f * <:F:>) c= dom <:F:> & dom <:F:> c= (arity F) -tuples_on D ) by Th45, RELAT_1:44;
hence A1: dom (f * <:F:>) c= (arity F) -tuples_on D by XBOOLE_1:1; :: thesis: ( rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
(arity F) -tuples_on D c= D * by MSUALG_1:12;
then A2: dom (f * <:F:>) c= D * by A1, XBOOLE_1:1;
( rng (f * <:F:>) c= rng f & rng f c= D ) by RELAT_1:45, RELAT_1:def 19;
hence rng (f * <:F:>) c= D by XBOOLE_1:1; :: thesis: f * <:F:> in HFuncs D
then f * <:F:> is PartFunc of (D * ),D by A2, RELSET_1:11;
then f * <:F:> in PFuncs (D * ),D by PARTFUN1:119;
hence f * <:F:> in HFuncs D ; :: thesis: verum