let x1, x2, x3 be set ; :: thesis: for D, D' being non empty set
for p being FinSequence of D
for f being Function of D,D' st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let D, D' be non empty set ; :: thesis: for p being FinSequence of D
for f being Function of D,D' st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let p be FinSequence of D; :: thesis: for f being Function of D,D' st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let f be Function of D,D'; :: thesis: ( p = <*x1,x2,x3*> implies f * p = <*(f . x1),(f . x2),(f . x3)*> )
assume A1: p = <*x1,x2,x3*> ; :: thesis: f * p = <*(f . x1),(f . x2),(f . x3)*>
reconsider q = f * p as FinSequence of D' by Th36;
len p = 3 by A1, FINSEQ_1:62;
then A2: len q = 3 by Th37;
then ( 1 in Seg (len q) & 2 in Seg (len q) & 3 in Seg (len q) ) ;
then ( 1 in dom q & 2 in dom q & 3 in dom q & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 ) by A1, FINSEQ_1:62, FINSEQ_1:def 3;
then ( q . 1 = f . x1 & q . 2 = f . x2 & q . 3 = f . x3 ) by FUNCT_1:22;
hence f * p = <*(f . x1),(f . x2),(f . x3)*> by A2, FINSEQ_1:62; :: thesis: verum