let D be non empty set ; for F being with_the_same_arity FinSequence of HFuncs D holds dom <:F:> c= (arity F) -tuples_on D
set X = D;
let F be with_the_same_arity FinSequence of HFuncs D; dom <:F:> c= (arity F) -tuples_on D
thus
dom <:F:> c= (arity F) -tuples_on D
verumproof
A1:
dom <:F:> =
meet (doms F)
by FUNCT_6:29
.=
meet (rng (doms F))
by FUNCT_6:def 4
;
let x be
object ;
TARSKI:def 3 ( not x in dom <:F:> or x in (arity F) -tuples_on D )
assume A2:
x in dom <:F:>
;
x in (arity F) -tuples_on D
consider y being
object such that A3:
y in rng (doms F)
by A2, A1, SETFAM_1:1, XBOOLE_0:def 1;
reconsider y =
y as
set by TARSKI:1;
A4:
x in y
by A2, A1, A3, SETFAM_1:def 1;
consider z being
object such that A5:
z in dom (doms F)
and A6:
(doms F) . z = y
by A3, FUNCT_1:def 3;
A7:
dom (doms F) = dom F
by FUNCT_6:def 2;
then
z in dom F
by A5;
then A8:
F . z in rng F
by FUNCT_1:3;
rng F c= HFuncs D
by RELAT_1:def 19;
then reconsider Fz =
F . z as
Element of
HFuncs D by A8;
A9:
dom Fz c= (arity Fz) -tuples_on D
by Th19;
(doms F) . z = dom Fz
by A7, A5, FUNCT_6:def 2;
then
x in (arity Fz) -tuples_on D
by A6, A4, A9;
hence
x in (arity F) -tuples_on D
by A8, Def4;
verum
end;