let n be Nat; :: thesis: for p, q being FinSequence st 1 <= n & n <= len p holds
p . n = (p ^ q) . n
let p, q be FinSequence; :: thesis: ( 1 <= n & n <= len p implies p . n = (p ^ q) . n )
assume ( 1 <= n & n <= len p ) ; :: thesis: p . n = (p ^ q) . n
then n in dom p by FINSEQ_3:25;
hence p . n = (p ^ q) . n by FINSEQ_1:def 7; :: thesis: verum