let p, q be FinSequence; :: thesis: for i being Nat st 1 <= i & i <= len p holds
(p ^ q) . i = p . i
let i be Nat; :: thesis: ( 1 <= i & i <= len p implies (p ^ q) . i = p . i )
A1: i in NAT by ORDINAL1:def 13;
assume A2: ( 1 <= i & i <= len p ) ; :: thesis: (p ^ q) . i = p . i
Seg (len p) = dom p by Def3;
then i in dom p by A1, A2;
hence (p ^ q) . i = p . i by Def7; :: thesis: verum