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