let f be Function; :: thesis: for x, y being set st x in dom f & y in dom f holds
f * <*x,y*> = <*(f . x),(f . y)*>
let x, y be set ; :: thesis: ( x in dom f & y in dom f implies f * <*x,y*> = <*(f . x),(f . y)*> )
assume that
A1: x in dom f and
A2: y in dom f ; :: thesis: f * <*x,y*> = <*(f . x),(f . y)*>
reconsider D = dom f, E = rng f as non empty set by A1, FUNCT_1:3;
rng <*x,y*> = {x,y} by Lm1;
then rng <*x,y*> c= D by A1, A2, ZFMISC_1:32;
then reconsider p = <*x,y*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1, RELSET_1:4;
thus f * <*x,y*> = g * p
.= <*(f . x),(f . y)*> by Th34 ; :: thesis: verum