let f be Function; :: thesis: for x, y, z being set st x in dom f & y in dom f & z in dom f holds
f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
let x, y, z be set ; :: thesis: ( x in dom f & y in dom f & z in dom f implies f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*> )
assume that
A1: x in dom f and
A2: ( y in dom f & z in dom f ) ; :: thesis: f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
reconsider D = dom f, E = rng f as non empty set by A1, FUNCT_1:3;
rng <*x,y,z*> = {x,y,z} by Lm2;
then A3: rng <*x,y,z*> = {x,y} \/ {z} by ENUMSET1:3;
( {x,y} c= D & {z} c= D ) by A1, A2, ZFMISC_1:31, ZFMISC_1:32;
then rng <*x,y,z*> c= D by A3, XBOOLE_1:8;
then reconsider p = <*x,y,z*> 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,z*> = g * p
.= <*(f . x),(f . y),(f . z)*> by Th35 ; :: thesis: verum