let p be non empty FinSequence; :: thesis: for q being FinSequence
for i being natural number st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let q be FinSequence; :: thesis: for i being natural number st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let i be natural number ; :: thesis: ( i < len q implies (p $^ q) . ((len p) + i) = q . (i + 1) )
assume A1: i < len q ; :: thesis: (p $^ q) . ((len p) + i) = q . (i + 1)
then consider j being Element of NAT , r being FinSequence such that
A2: ( len p = j + 1 & r = p | (Seg j) & p $^ q = r ^ q ) by CARD_1:47, REWRITE1:def 1;
j < len p by A2, NAT_1:13;
then ( len r = j & i + 1 >= 1 & i + 1 <= len q & i + 1 is Element of NAT ) by A1, A2, FINSEQ_1:21, NAT_1:11, NAT_1:13;
then ( (len p) + i = (len r) + (i + 1) & i + 1 in dom q ) by A2, FINSEQ_3:27;
hence (p $^ q) . ((len p) + i) = q . (i + 1) by A2, FINSEQ_1:def 7; :: thesis: verum