let f be Function; :: thesis: for x1, x2, x3, x4, x5 being set st x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f holds
f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*>
let x1, x2, x3, x4, x5 be set ; :: thesis: ( x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f implies f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> )
assume A1: ( x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f ) ; :: thesis: f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*>
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:12;
reconsider g = f as Function of D,E by FUNCT_2:def 1, RELSET_1:11;
rng <*x1,x2,x3,x4,x5*> c= D

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng <*x1,x2,x3,x4,x5*> or a in D )
assume a in rng <*x1,x2,x3,x4,x5*> ; :: thesis: a in D
then a in {x1,x2,x3,x4,x5} by Th15;
hence a in D by A1, ENUMSET1:def 3; :: thesis: verum

end;

then reconsider p = <*x1,x2,x3,x4,x5*> as FinSequence of D by FINSEQ_1:def 4;
A2: ( dom (g * p) = dom p & len (g * p) = len p & ( for n being Element of NAT st n in dom (g * p) holds
(g * p) . n = g . (p . n) ) ) by ALG_1:1;
then A3: dom (g * p) = Seg 5 by FINSEQ_4:94
.= dom <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> by FINSEQ_4:94 ;

now

let k be Nat; :: thesis: ( k in dom (g * p) implies (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁ )
assume A4: k in dom (g * p) ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁
then A5: k in Seg 5 by A2, FINSEQ_4:94;

per cases ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A5, ENUMSET1:def 3, FINSEQ_3:3;

suppose A6: k = 1 ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁

then p . k = x1 by FINSEQ_4:93;
then (g * p) . k = g . x1 by A4, ALG_1:1;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A6, FINSEQ_4:93; :: thesis: verum

end;

suppose A7: k = 2 ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁

then p . k = x2 by FINSEQ_4:93;
then (g * p) . k = g . x2 by A4, ALG_1:1;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A7, FINSEQ_4:93; :: thesis: verum

end;

suppose A8: k = 3 ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁

then p . k = x3 by FINSEQ_4:93;
then (g * p) . k = g . x3 by A4, ALG_1:1;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A8, FINSEQ_4:93; :: thesis: verum

end;

suppose A9: k = 4 ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁

then p . k = x4 by FINSEQ_4:93;
then (g * p) . k = g . x4 by A4, ALG_1:1;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A9, FINSEQ_4:93; :: thesis: verum

end;

suppose A10: k = 5 ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁

then p . k = x5 by FINSEQ_4:93;
then (g * p) . k = g . x5 by A4, ALG_1:1;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A10, FINSEQ_4:93; :: thesis: verum

end;

end;

end;

hence f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> by A3, FINSEQ_1:17; :: thesis: verum