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) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1 )
assume A5: k in dom (g * p) ; :: thesis: (g * p) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
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) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
then p . k = x1 by FINSEQ_4:78;
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, FINSEQ_4:78; :: thesis: verum
end;
suppose A8: k = 2 ; :: thesis: (g * p) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
then p . k = x2 by FINSEQ_4:78;
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, FINSEQ_4:78; :: thesis: verum
end;
suppose A9: k = 3 ; :: thesis: (g * p) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
then p . k = x3 by FINSEQ_4:78;
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, FINSEQ_4:78; :: thesis: verum
end;
suppose A10: k = 4 ; :: thesis: (g * p) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
then p . k = x4 by FINSEQ_4:78;
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, FINSEQ_4:78; :: thesis: verum
end;
suppose A11: k = 5 ; :: thesis: (g * p) . b1 = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*> . b1
then p . k = x5 by FINSEQ_4:78;
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, FINSEQ_4:78; :: 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