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 } ;

per cases ( f = {} or F = {} or ex h being set st
( h in rng F & h = {} ) or ( F <> {} & f <> {} & ( for h being set st h in rng F holds
h <> {} ) ) ) ;

suppose f = {} ; :: thesis: f * <:F:> is quasi_total Element of HFuncs D

hence f * <:F:> is quasi_total Element of HFuncs D ; :: thesis: verum

end;

suppose F = {} ; :: thesis: f * <:F:> is quasi_total Element of HFuncs D

hence f * <:F:> is quasi_total Element of HFuncs D by A4, A3, FUNCT_6:40; :: thesis: verum

end;

suppose ex h being set st
( h in rng F & h = {} ) ; :: thesis: f * <:F:> is quasi_total Element of HFuncs D

then <:F:> = {} by Th7;
hence f * <:F:> is quasi_total Element of HFuncs D by A4, A3; :: thesis: verum

end;

suppose A5: ( F <> {} & f <> {} & ( for h being set st h in rng F holds
h <> {} ) ) ; :: thesis: f * <:F:> is quasi_total Element of HFuncs D

then for h being Element of HFuncs D st h in rng F holds
( h is quasi_total & not h is empty ) by A2;
hence f * <:F:> is quasi_total Element of HFuncs D by A1, A5, Th44; :: thesis: verum

end;

end;