let X be set ; for Y being non empty set
for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y
let Y be non empty set ; for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y
let p be FinSequence of X; ((X --> Y) #) . p = (len p) -tuples_on Y
rng p c= X
by FINSEQ_1:def 4;
then
(rng p) /\ X = rng p
by XBOOLE_1:28;
then A1: p " X =
p " (rng p)
by RELAT_1:133
.=
dom p
by RELAT_1:134
;
p in X *
by FINSEQ_1:def 11;
hence ((X --> Y) #) . p =
product ((X --> Y) * p)
by FINSEQ_2:def 5
.=
product ((p " X) --> Y)
by FUNCOP_1:19
.=
product ((Seg (len p)) --> Y)
by A1, FINSEQ_1:def 3
.=
(len p) -tuples_on Y
by Lm1
;
verum