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