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 that
A1: x1 in dom f and
A2: ( 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)*>
reconsider D = dom f, E = rng f as non empty set by A1, FUNCT_1:3;
rng <*x1,x2,x3,x4,x5*> c= D

proof

let a be object ; :: 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 Th14;
hence a in D by A1, A2, ENUMSET1:def 3; :: thesis: verum

end;

then reconsider p = <*x1,x2,x3,x4,x5*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1, RELSET_1:4;
A3: dom (g * p) = dom p by FINSEQ_3:120;

A4: now :: thesis: for k being Nat st k in dom (g * p) holds
(g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k

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 A5: k in dom (g * p) ; :: thesis: (g * p) . b₁ = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b₁
then A6: k in Seg 5 by A3, FINSEQ_1:89;

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

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

then p . k = x1 ;
then (g * p) . k = g . x1 by A5, FINSEQ_3:120;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A7; :: thesis: verum

end;

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

then p . k = x2 ;
then (g * p) . k = g . x2 by A5, FINSEQ_3:120;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A8; :: thesis: verum

end;

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

then p . k = x3 ;
then (g * p) . k = g . x3 by A5, FINSEQ_3:120;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A9; :: thesis: verum

end;

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

then p . k = x4 ;
then (g * p) . k = g . x4 by A5, FINSEQ_3:120;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A10; :: thesis: verum

end;

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

then p . k = x5 ;
then (g * p) . k = g . x5 by A5, FINSEQ_3:120;
hence (g * p) . k = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . k by A11; :: thesis: verum

end;

end;

end;

dom (g * p) = Seg 5 by A3, FINSEQ_1:89
.= dom <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> by FINSEQ_1:89 ;
hence f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> by A4, FINSEQ_1:13; :: thesis: verum