let n be Element of 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 ( 1 <= n & n <= len p ) ; :: thesis: (p ^ q) . n = p . n
then n in dom p by FINSEQ_3:27;
hence (p ^ q) . n = p . n by FINSEQ_1:def 7; :: thesis: verum