let x1, x2, x3 be object ; :: thesis: for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let D, D9 be non empty set ; :: thesis: for p being FinSequence of D
for f being Function of D,D9 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,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let f be Function of D,D9; :: 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)*>
A2: p . 2 = x2 by A1, FINSEQ_1:45;
reconsider q = f * p as FinSequence of D9 by Th30;
len p = 3 by A1, FINSEQ_1:45;
then A3: len q = 3 by Th31;
then 2 in Seg (len q) ;
then 2 in dom q by FINSEQ_1:def 3;
then A4: q . 2 = f . x2 by A2, FUNCT_1:12;
A5: p . 3 = x3 by A1, FINSEQ_1:45;
A6: p . 1 = x1 by A1, FINSEQ_1:45;
3 in Seg (len q) by A3;
then 3 in dom q by FINSEQ_1:def 3;
then A7: q . 3 = f . x3 by A5, FUNCT_1:12;
1 in Seg (len q) by A3;
then 1 in dom q by FINSEQ_1:def 3;
then q . 1 = f . x1 by A6, FUNCT_1:12;
hence f * p = <*(f . x1),(f . x2),(f . x3)*> by A3, A4, A7, FINSEQ_1:45; :: thesis: verum