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
set fF = f * <:F:>;
reconsider g = {} as PartFunc of (D * ),D by RELSET_1:25;
g in PFuncs (D * ),D by PARTFUN1:119;
then A3: g in { h where h is Element of PFuncs (D * ),D : h is homogeneous } ;
A4: g is quasi_total

proof

let x, y be FinSequence of D; :: according to UNIALG_1:def 2 :: thesis: ( not len x = len y or not x in dom g or y in dom g )
assume ( len x = len y & x in dom g ) ; :: thesis: y in dom g
hence y in dom g ; :: thesis: verum

end;

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

then f * <:F:> = f * {} by FUNCT_6:60;
hence f * <:F:> is quasi_total Element of HFuncs D by A3, A4; :: 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 Th10;
hence f * <:F:> is quasi_total Element of HFuncs D by A3, A4; :: 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, Th49; :: thesis: verum

end;

end;