let p be non empty FinSequence; :: thesis: for q being FinSequence
for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let q be FinSequence; :: thesis: for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let i be Nat; :: thesis: ( i < len q implies (p $^ q) . ((len p) + i) = q . (i + 1) )
A1: i + 1 >= 1 by NAT_1:11;
assume A2: i < len q ; :: thesis: (p $^ q) . ((len p) + i) = q . (i + 1)
then consider j being Nat, r being FinSequence such that
A3: len p = j + 1 and
A4: r = p | (Seg j) and
A5: p $^ q = r ^ q by CARD_1:27, REWRITE1:def 1;
i + 1 <= len q by A2, NAT_1:13;
then A6: i + 1 in dom q by A1, FINSEQ_3:25;
j < len p by A3, NAT_1:13;
then len r = j by A4, FINSEQ_1:17;
then (len p) + i = (len r) + (i + 1) by A3;
hence (p $^ q) . ((len p) + i) = q . (i + 1) by A5, A6, FINSEQ_1:def 7; :: thesis: verum