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

proof

let x, y be FinSequence of D; :: according to MARGREL1:def 22 :: thesis: ( not len x = len y or not x in proj1 g or y in proj1 g )
assume that
len x = len y and
A4: x in dom g ; :: thesis: y in proj1 g
thus y in dom g by A4; :: thesis: verum

end;

g in PFuncs ((D *),D) by PARTFUN1:45;
then A5: 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 A5, 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 Th10;
hence f * <:F:> is quasi_total Element of HFuncs D by A5, A3; :: thesis: verum

end;

suppose A6: ( 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, A6, Th49; :: thesis: verum

end;

end;