let D be non empty set ; :: thesis: 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; :: thesis: dom <:F:> c= (arity F) -tuples_on D
thus
dom <:F:> c= (arity F) -tuples_on D
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in dom <:F:> or x in (arity F) -tuples_on D )
assume A1:
x in dom <:F:>
;
:: thesis: x in (arity F) -tuples_on D
A2:
dom <:F:> =
meet (doms F)
by FUNCT_6:49
.=
meet (rng (doms F))
by FUNCT_6:def 4
;
A3:
dom (doms F) = F " (SubFuncs (rng F))
by FUNCT_6:def 2;
consider y being
set such that A4:
y in rng (doms F)
by A1, A2, SETFAM_1:2, XBOOLE_0:def 1;
consider z being
set such that A5:
(
z in dom (doms F) &
(doms F) . z = y )
by A4, FUNCT_1:def 5;
z in dom F
by A3, A5, FUNCT_6:28;
then A6:
(
F . z in rng F &
rng F c= HFuncs D )
by FUNCT_1:12, RELAT_1:def 19;
then reconsider Fz =
F . z as
Element of
HFuncs D ;
A7:
(doms F) . z = dom Fz
by A3, A5, FUNCT_6:def 2;
A8:
x in y
by A1, A2, A4, SETFAM_1:def 1;
dom Fz c= (arity Fz) -tuples_on D
by Th23;
then
x in (arity Fz) -tuples_on D
by A5, A7, A8;
hence
x in (arity F) -tuples_on D
by A6, Def7;
:: thesis: verum
end;