let i be Nat; :: thesis: for f being FinSequence st i in dom f holds
(App <*f*>) . <*i*> = <*(f . i)*>
let f be FinSequence; :: thesis: ( i in dom f implies (App <*f*>) . <*i*> = <*(f . i)*> )
set I = <*i*>;
set A = App <*f*>;
A1: ( len <*i*> = 1 & <*i*> . 1 = i ) by FINSEQ_1:40;
assume i in dom f ; :: thesis: (App <*f*>) . <*i*> = <*(f . i)*>
then A2: <*i*> in doms <*f*> by A1, Th51;
A3: 1 in dom <*i*> by A1, FINSEQ_3:25;
(<*f*> . 1) . (<*i*> . 1) = f . i ;
then ((App <*f*>) . <*i*>) . 1 = f . i by A3, A2, Def9;
hence (App <*f*>) . <*i*> = <*(f . i)*> by A2, A1, Def9, FINSEQ_1:40; :: thesis: verum