let f be Function; :: thesis: for x1, x2, x3, x4 being set st x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f holds
f * <*x1,x2,x3,x4*> = <*(f . x1),(f . x2),(f . x3),(f . x4)*>
let x1, x2, x3, x4 be set ; :: thesis: ( x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f implies f * <*x1,x2,x3,x4*> = <*(f . x1),(f . x2),(f . x3),(f . x4)*> )
assume A1: ( x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f ) ; :: thesis: f * <*x1,x2,x3,x4*> = <*(f . x1),(f . x2),(f . x3),(f . x4)*>
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*> c= D

proof

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

end;

then reconsider p = <*x1,x2,x3,x4*> 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 4 by FINSEQ_4:92
.= dom <*(f . x1),(f . x2),(f . x3),(f . x4)*> by FINSEQ_4:92 ;

now

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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