let f be Function; :: thesis: for x being set st x in dom f holds
f * <*x*> = <*(f . x)*>
let x be set ; :: thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )
assume A1: x in dom f ; :: thesis: f * <*x*> = <*(f . x)*>
then f . x in rng f by FUNCT_1:def 5;
then reconsider D = dom f, E = rng f as non empty set by A1;
reconsider g = f as Function of D,E by FUNCT_2:def 1, RELSET_1:11;
rng <*x*> = {x} by FINSEQ_1:55;
then rng <*x*> c= D by A1, ZFMISC_1:37;
then reconsider p = <*x*> as FinSequence of D by FINSEQ_1:def 4;
thus f * <*x*> = g * p
.= <*(f . x)*> by FINSEQ_2:39 ; :: thesis: verum