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

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