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 and
A2: not F is empty and
A3: for h being Element of HFuncs D st h in rng F holds
( h is quasi_total & not h is empty ) ; :: thesis:
set n = arity F;
set fF = f * <:F:>;
A4: dom (f * <:F:>) c= (arity F) -tuples_on D by Th41;
A5: (arity F) -tuples_on D c= dom (f * <:F:>)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A6: product (rngs F) c= (len F) -tuples_on D

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
A7: dom (rngs F) = dom F by FUNCT_6:def 3;
assume p in product (rngs F) ; :: thesis:
then consider g being Function such that
A8: p = g and
A9: dom g = dom (rngs F) and
A10: for x being object st x in dom (rngs F) holds
g . x in (rngs F) . x by CARD_3:def 5;
A11: dom F = Seg (len F) by FINSEQ_1:def 3;
then reconsider g = g as FinSequence by A9, A7, FINSEQ_1:def 2;
rng g c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider d being object such that
A12: d in dom g and
A13: g . d = x by FUNCT_1:def 3;
A14: g . d in (rngs F) . d by A9, A10, A12;
reconsider d = d as Element of NAT by A12;
reconsider Fd = F . d as Element of HFuncs D by A9, A7, A12, FINSEQ_2:11;
A15: rng Fd c= D by RELAT_1:def 19;
(rngs F) . d = rng Fd by A9, A7, A12, FUNCT_6:def 3;
hence x in D by A13, A14, A15; :: thesis:

end;

then reconsider g = g as FinSequence of D by FINSEQ_1:def 4;
len g = len F by A9, A7, A11, FINSEQ_1:def 3;
then p is Element of (len F) -tuples_on D by A8, FINSEQ_2:92;
hence p in (len F) -tuples_on D ; :: thesis:

end;

rng <:F:> c= product (rngs F) by FUNCT_6:29;
then A16: rng <:F:> c= (len F) -tuples_on D by A6;
A17: dom f = (arity f) -tuples_on D by Th21;
A18: (arity F) -tuples_on D c= dom <:F:>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A19: dom (doms F) = dom F by FUNCT_6:def 2;
assume A20: x in (arity F) -tuples_on D ; :: thesis:

A21: now :: thesis:

let y be set ; :: thesis:
assume y in rng (doms F) ; :: thesis:
then consider w being object such that
A22: w in dom (doms F) and
A23: (doms F) . w = y by FUNCT_1:def 3;
A24: w in dom F by A19, A22;
then reconsider w = w as Element of NAT ;
reconsider Fw = F . w as Element of HFuncs D by A24, FINSEQ_2:11;
A25: (doms F) . w = dom Fw by A19, A22, FUNCT_6:def 2;
A26: Fw in rng F by A24, FUNCT_1:3;
then ( not Fw is empty & Fw is quasi_total ) by A3;
then dom Fw = (arity Fw) -tuples_on D by Th21;
hence x in y by A20, A23, A25, A26, Def4; :: thesis:

end;

consider z being object such that
A27: z in dom F by A2, XBOOLE_0:def 1;
z in dom (doms F) by A27, A19;
then A28: rng (doms F) <> {} by RELAT_1:42;
dom <:F:> = meet (doms F) by FUNCT_6:29
.= meet (rng (doms F)) by FUNCT_6:def 4 ;
hence x in dom <:F:> by A28, A21, SETFAM_1:def 1; :: thesis:

end;

assume A29: x in (arity F) -tuples_on D ; :: thesis:
then <:F:> . x in rng <:F:> by A18, FUNCT_1:3;
hence x in dom (f * <:F:>) by A1, A29, A18, A17, A16, FUNCT_1:11; :: thesis:

end;

then A30: dom (f * <:F:>) = (arity F) -tuples_on D by A4, XBOOLE_0:def 10;
A31: rng (f * <:F:>) c= D by Th41;
(arity F) -tuples_on D c= D * by FINSEQ_2:142;
then dom (f * <:F:>) c= D * by A4;
then f * <:F:> is Relation of (D *),D by A31, RELSET_1:4;
then f * <:F:> is Element of PFuncs ((D *),D) by PARTFUN1:45;
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 MARGREL1:def 22 :: thesis:
assume that
A32: len x = len y and
A33: x in dom fF ; :: thesis:
len x = arity F by A4, A33, CARD_1:def 7;
then y is Element of (arity F) -tuples_on D by A32, FINSEQ_2:92;
hence y in dom fF by A30; :: thesis:

end;

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