let p, q be FinSequence; :: thesis: for i being Nat st i >= 1 & i < len p holds
(p $^ q) . i = p . i
let i be Nat; :: thesis: ( i >= 1 & i < len p implies (p $^ q) . i = p . i )
assume that
A1: i >= 1 and
A2: i < len p ; :: thesis: (p $^ q) . i = p . i

per cases ( q = {} or q <> {} ) ;

suppose q = {} ; :: thesis: (p $^ q) . i = p . i

hence (p $^ q) . i = p . i by REWRITE1:1; :: thesis: verum

end;

suppose q <> {} ; :: thesis: (p $^ q) . i = p . i

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 A2, CARD_1:27, REWRITE1:def 1;
A6: p = r ^ <*(p . (len p))*> by A3, A4, FINSEQ_3:55;
j < len p by A3, NAT_1:13;
then A7: len r = j by A4, FINSEQ_1:17;
i <= j by A2, A3, NAT_1:13;
then A8: i in dom r by A1, A7, FINSEQ_3:25;
then (p $^ q) . i = r . i by A5, FINSEQ_1:def 7;
hence (p $^ q) . i = p . i by A8, A6, FINSEQ_1:def 7; :: thesis: verum

end;

end;