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

end;

end;