let X be set ; :: thesis: 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 ; :: thesis: for p being FinSequence of X holds ((X --> Y) # ) . p = (len p) -tuples_on Y
let p be FinSequence of X; :: thesis: ((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:168
.= dom p by RELAT_1:169 ;
p in X * by FINSEQ_1:def 11;
hence ((X --> Y) # ) . p = product ((X --> Y) * p) by PBOOLE:def 19
.= product ((p " X) --> Y) by FUNCOP_1:25
.= product ((Seg (len p)) --> Y) by A1, FINSEQ_1:def 3
.= (len p) -tuples_on Y by Lm1 ;
:: thesis: verum