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 Th46;
A5: (arity F) -tuples_on D c= dom (f * <:F:>)

proof

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

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
A7: dom (rngs F) = F " (SubFuncs (rng 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 set st x in dom (rngs F) holds
g . x in (rngs F) . x by CARD_3:def 5;

now

let x be set ; :: thesis:

hereby :: thesis:

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

end;

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

end;

then A13: F " (SubFuncs (rng F)) = Seg (len F) by TARSKI:2;
then reconsider g = g as FinSequence by A9, A7, 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
A14: d in dom g and
A15: g . d = x by FUNCT_1:def 5;
A16: g . d in (rngs F) . d by A9, A10, A14;
reconsider d = d as Element of NAT by A14;
dom F = Seg (len F) by FINSEQ_1:def 3;
then reconsider Fd = F . d as Element of HFuncs D by A9, A7, A13, A14, FINSEQ_2:13;
A17: rng Fd c= D by RELAT_1:def 19;
(rngs F) . d = rng Fd by A9, A7, A14, FUNCT_6:def 3;
hence x in D by A15, A16, A17; :: thesis:

end;

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

end;

rng <:F:> c= product (rngs F) by FUNCT_6:49;
then A18: rng <:F:> c= (len F) -tuples_on D by A6, XBOOLE_1:1;
A19: dom f = (arity f) -tuples_on D by Th25;
A20: (arity F) -tuples_on D c= dom <:F:>

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
A22: dom (doms F) = F " (SubFuncs (rng F)) by FUNCT_6:def 2;
assume A23: x in (arity F) -tuples_on D ; :: thesis:

A24: now

let y be set ; :: thesis:
assume y in rng (doms F) ; :: thesis:
then consider w being set such that
A25: w in dom (doms F) and
A26: (doms F) . w = y by FUNCT_1:def 5;
A27: w in dom F by A22, A25, FUNCT_6:28;
then reconsider w = w as Element of NAT ;
reconsider Fw = F . w as Element of HFuncs D by A27, FINSEQ_2:13;
A28: (doms F) . w = dom Fw by A22, A25, FUNCT_6:def 2;
A29: Fw in rng F by A27, FUNCT_1:12;
then ( not Fw is empty & Fw is quasi_total ) by A3;
then dom Fw = (arity Fw) -tuples_on D by Th25;
hence x in y by A23, A26, A28, A29, Def7; :: thesis:

end;

consider z being set such that
A30: z in dom F by A2, XBOOLE_0:def 1;
F . z in rng F by A30, FUNCT_1:12;
then z in dom (doms F) by A30, A22, FUNCT_6:28;
then A31: rng (doms F) <> {} by RELAT_1:65;
dom <:F:> = meet (doms F) by FUNCT_6:49
.= meet (rng (doms F)) by FUNCT_6:def 4 ;
hence x in dom <:F:> by A31, A24, SETFAM_1:def 1; :: thesis:

end;

assume A32: x in (arity F) -tuples_on D ; :: thesis:
then <:F:> . x in rng <:F:> by A20, FUNCT_1:12;
hence x in dom (f * <:F:>) by A1, A32, A20, A19, A18, FUNCT_1:21; :: thesis:

end;

then A33: dom (f * <:F:>) = (arity F) -tuples_on D by A4, XBOOLE_0:def 10;
A34: rng (f * <:F:>) c= D by Th46;
(arity F) -tuples_on D c= D * by FINSEQ_2:162;
then dom (f * <:F:>) c= D * by A4, XBOOLE_1:1;
then f * <:F:> is Relation of (D * ),D by A34, 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 MARGREL1:def 23 :: thesis:
assume that
A35: len x = len y and
A36: x in dom fF ; :: thesis:
len x = arity F by A4, A36, FINSEQ_1:def 18;
then y is Element of (arity F) -tuples_on D by A35, FINSEQ_2:110;
hence y in dom fF by A33; :: 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: