let x be set ; :: thesis: for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>
let f be Function; :: thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )
assume A1: x in dom f ; :: thesis: f * <*x*> = <*(f . x)*>
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:3;
rng <*x*> = {x} by FINSEQ_1:38;
then rng <*x*> c= D by A1, ZFMISC_1:31;
then reconsider p = <*x*> as FinSequence of D by FINSEQ_1:def 4;
reconsider f = f as Function of D,E by FUNCT_2:def 1, RELSET_1:4;
reconsider q = f * p as FinSequence of E by Th30;
A2: p . 1 = x by FINSEQ_1:40;
A3: len q = len p by Th31
.= 1 by FINSEQ_1:39 ;
then 1 in Seg (len q) ;
then 1 in dom q by FINSEQ_1:def 3;
then q . 1 = f . x by A2, FUNCT_1:12;
hence f * <*x*> = <*(f . x)*> by A3, FINSEQ_1:40; :: thesis: verum