let D be non empty set ; :: thesis:
set X = D;
let f be non empty quasi_total Element of HFuncs D; :: thesis:
let F be with_the_same_arity FinSequence of HFuncs D; :: thesis:
assume that
A1: ( arity f = len F & not F is empty ) and
A2: for h being Element of HFuncs D st h in rng F holds
( h is quasi_total & not h is empty ) ; :: thesis:
set fF = f * <:F:>;
set n = arity F;
A3: dom (f * <:F:>) c= (arity F) -tuples_on D by Th46;
A4: (arity F) -tuples_on D c= dom (f * <:F:>)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in (arity F) -tuples_on D ; :: thesis:
A6: (arity F) -tuples_on D c= dom <:F:>

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in (arity F) -tuples_on D ; :: thesis:
A8: dom <:F:> = meet (doms F) by FUNCT_6:49
.= meet (rng (doms F)) by FUNCT_6:def 4 ;
dom F <> {} by A1;
then consider z being set such that
A9: z in dom F by XBOOLE_0:def 1;
( F . z in rng F & rng F c= HFuncs D ) by A9, FINSEQ_1:def 4, FUNCT_1:12;
then A10: F . z is Element of HFuncs D ;
A11: dom (doms F) = F " (SubFuncs (rng F)) by FUNCT_6:def 2;
then z in dom (doms F) by A9, A10, FUNCT_6:28;
then A12: rng (doms F) <> {} by RELAT_1:65;

now

let y be set ; :: thesis:
assume y in rng (doms F) ; :: thesis:
then consider w being set such that
A13: ( w in dom (doms F) & (doms F) . w = y ) by FUNCT_1:def 5;
A14: w in dom F by A11, A13, FUNCT_6:28;
then reconsider w = w as Element of NAT ;
reconsider Fw = F . w as Element of HFuncs D by A14, FINSEQ_2:13;
A15: (doms F) . w = dom Fw by A11, A13, FUNCT_6:def 2;
A16: Fw in rng F by A14, FUNCT_1:12;
then ( not Fw is empty & Fw is quasi_total ) by A2;
then dom Fw = (arity Fw) -tuples_on D by Th25;
hence x in y by A7, A13, A15, A16, Def7; :: thesis:

end;

hence x in dom <:F:> by A8, A12, SETFAM_1:def 1; :: thesis:

end;

A17: dom f = (arity f) -tuples_on D by Th25;
A18: rng <:F:> c= product (rngs F) by FUNCT_6:49;
product (rngs F) c= (len F) -tuples_on D

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in product (rngs F) ; :: thesis:
then consider g being Function such that
A19: ( p = g & dom g = dom (rngs F) ) and
A20: for x being set st x in dom (rngs F) holds
g . x in (rngs F) . x by CARD_3:def 5;
A21: dom (rngs F) = F " (SubFuncs (rng F)) by FUNCT_6:def 3;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in F " (SubFuncs (rng F)) ; :: thesis:
then ( x in dom F & dom F = Seg (len F) ) by FINSEQ_1:def 3, FUNCT_6:28;
hence x in Seg (len F) ; :: thesis:

end;

assume x in Seg (len F) ; :: thesis:
then A22: x in dom F by FINSEQ_1:def 3;
then ( F . x in rng F & rng F c= HFuncs D ) by FINSEQ_1:def 4, FUNCT_1:12;
then F . x is Element of HFuncs D ;
hence x in F " (SubFuncs (rng F)) by A22, FUNCT_6:28; :: thesis:

end;

then A23: F " (SubFuncs (rng F)) = Seg (len F) by TARSKI:2;
then reconsider g = g as FinSequence by A19, A21, FINSEQ_1:def 2;
rng g c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider d being set such that
A24: ( d in dom g & g . d = x ) by FUNCT_1:def 5;
A25: g . d in (rngs F) . d by A19, A20, A24;
A26: dom F = Seg (len F) by FINSEQ_1:def 3;
reconsider d = d as Element of NAT by A24;
reconsider Fd = F . d as Element of HFuncs D by A19, A21, A23, A24, A26, FINSEQ_2:13;
A27: (rngs F) . d = rng Fd by A19, A21, A24, FUNCT_6:def 3;
rng Fd c= D by RELAT_1:def 19;
hence x in D by A24, A25, A27; :: thesis:

end;

then reconsider g = g as FinSequence of D by FINSEQ_1:def 4;
len g = len F by A19, A21, A23, FINSEQ_1:def 3;
then p is Element of (len F) -tuples_on D by A19, FINSEQ_2:110;
hence p in (len F) -tuples_on D ; :: thesis:

end;

then ( <:F:> . x in rng <:F:> & rng <:F:> c= (len F) -tuples_on D ) by A5, A6, A18, FUNCT_1:12, XBOOLE_1:1;
hence x in dom (f * <:F:>) by A1, A5, A6, A17, FUNCT_1:21; :: thesis:

end;

then A28: dom (f * <:F:>) = (arity F) -tuples_on D by A3, XBOOLE_0:def 10;
(arity F) -tuples_on D c= D * by MSUALG_1:12;
then A29: dom (f * <:F:>) c= D * by A3, XBOOLE_1:1;
rng (f * <:F:>) c= D by Th46;
then f * <:F:> is Relation of (D * ),D by A29, RELSET_1:11;
then f * <:F:> is Element of PFuncs (D * ),D by PARTFUN1:119;
then f * <:F:> in HFuncs D ;
then reconsider fF = f * <:F:> as Element of HFuncs D ;
fF is quasi_total

proof

let x, y be FinSequence of D; :: according to UNIALG_1:def 2 :: thesis:
assume A30: ( len x = len y & x in dom fF ) ; :: thesis:
len x = arity F by A3, A30, FINSEQ_1:def 18;
then y is Element of (arity F) -tuples_on D by A30, FINSEQ_2:110;
hence y in dom fF by A28; :: thesis:

end;

hence f * <:F:> is non empty quasi_total Element of HFuncs D by A4; :: thesis:
thus dom (f * <:F:>) = (arity F) -tuples_on D by A3, A4, XBOOLE_0:def 10; :: thesis: