let U1, U2 be non empty set ; :: thesis: for m being Nat
for p being U1 -valued b₁ -element FinSequence
for f being Function of U1,U2 holds f * p = (m -placesOf f) . p
let m be Nat; :: thesis: for p being U1 -valued m -element FinSequence
for f being Function of U1,U2 holds f * p = (m -placesOf f) . p
let p be U1 -valued m -element FinSequence; :: thesis: for f being Function of U1,U2 holds f * p = (m -placesOf f) . p
let f be Function of U1,U2; :: thesis: f * p = (m -placesOf f) . p
set F = m -placesOf f;
A1: ( dom f = U1 & dom (m -placesOf f) = m -tuples_on U1 & p in m -tuples_on U1 & f * p in m -tuples_on U2 ) by FUNCT_2:def 1, FOMODEL0:16;
reconsider pp = p as Element of m -tuples_on U1 by FOMODEL0:16;
pp is Element of Funcs ((Seg m),U1) by FOMODEL0:11;
then reconsider ppp = pp as Function of (Seg m),U1 ;
reconsider LH = f * p as Element of Funcs ((Seg m),U2) by FOMODEL0:11, A1;
reconsider RH = (m -placesOf f) . pp as Element of Funcs ((Seg m),U2) by FOMODEL0:11;
reconsider LHH = LH, RHH = RH as Function of (Seg m),U2 ;
reconsider LHHH = LH, RHHH = RH as Element of m -tuples_on U2 by FOMODEL0:11;
A2: ( dom ppp = Seg m & rng ppp c= U1 & dom LH = Seg m & dom LH = Seg m ) by FUNCT_2:def 1, RELAT_1:def 19;
[p,LH] in m -placesOf f

proof

for j being set st j in Seg m holds
[(pp . j),(LHHH . j)] in f

proof

let j be set ; :: thesis: ( j in Seg m implies [(pp . j),(LHHH . j)] in f )
assume A3: j in Seg m ; :: thesis: [(pp . j),(LHHH . j)] in f
then A4: LH . j = f . (p . j) by A2, FUNCT_1:12;
ppp . j in rng ppp by FUNCT_1:3, A3, A2;
hence [(pp . j),(LHHH . j)] in f by A1, A2, A4, FUNCT_1:1; :: thesis: verum

end;

hence [p,LH] in m -placesOf f ; :: thesis: verum

end;

hence f * p = (m -placesOf f) . p by FUNCT_1:1; :: thesis: verum