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

(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