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 )
assume A1: ( 1 <= i & i <= len p ) ; :: thesis: (p ^ q) . i = p . i
( i in NAT & Seg (len p) = dom p ) by Def3, ORDINAL1:def 12;
then i in dom p by A1;
hence (p ^ q) . i = p . i by Def7; :: thesis: verum