let U1, U2 be non empty set ; :: thesis: for m being Nat

for p being U1 -valued b_{1} -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

for p being U1 -valued b

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

hence
f * p = (m -placesOf f) . p
by FUNCT_1:1; :: thesis: verum
for j being set st j in Seg m holds

[(pp . j),(LHHH . j)] in f

end;[(pp . j),(LHHH . j)] in f

proof

hence
[p,LH] in m -placesOf f
; :: thesis: verum
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;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