let D be non empty set ; :: thesis: for f being quasi_total Element of HFuncs D
for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & ( for h being Element of HFuncs D st h in rng F holds
h is quasi_total ) holds
f * <:F:> is quasi_total Element of HFuncs D
set X = D;
let f be quasi_total Element of HFuncs D; :: thesis: for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & ( for h being Element of HFuncs D st h in rng F holds
h is quasi_total ) holds
f * <:F:> is quasi_total Element of HFuncs D
let F be with_the_same_arity FinSequence of HFuncs D; :: thesis: ( arity f = len F & ( for h being Element of HFuncs D st h in rng F holds
h is quasi_total ) implies f * <:F:> is quasi_total Element of HFuncs D )
assume that
A1: arity f = len F and
A2: for h being Element of HFuncs D st h in rng F holds
h is quasi_total ; :: thesis: f * <:F:> is quasi_total Element of HFuncs D
reconsider g = {} as PartFunc of (D *),D by RELSET_1:12;
A3: g is quasi_total ;
g in PFuncs ((D *),D) by PARTFUN1:45;
then A4: g in { h where h is Element of PFuncs ((D *),D) : h is homogeneous } ;