let i be Nat; :: thesis: for f, g being FinSequence st i <= len f holds
(f ^ g) | i = f | i
let f, g be FinSequence; :: thesis: ( i <= len f implies (f ^ g) | i = f | i )
assume A1: i <= len f ; :: thesis: (f ^ g) | i = f | i
then A2: len (f | i) = i by FINSEQ_1:59;
then A3: dom (f | i) = Seg i by FINSEQ_1:def 3;

A4: now :: thesis: for j being Nat st j in dom (f | i) holds
((f ^ g) | i) . j = (f | i) . j

let j be Nat; :: thesis: ( j in dom (f | i) implies ((f ^ g) | i) . j = (f | i) . j )
assume A5: j in dom (f | i) ; :: thesis: ((f ^ g) | i) . j = (f | i) . j
then j <= i by A3, FINSEQ_1:1;
then A6: j <= len f by A1, XXREAL_0:2;
( j in NAT & 1 <= j ) by A3, A5, FINSEQ_1:1;
then j in Seg (len f) by A6;
then A7: j in dom f by FINSEQ_1:def 3;
thus ((f ^ g) | i) . j = (f ^ g) . j by A3, A5, FUNCT_1:49
.= f . j by A7, FINSEQ_1:def 7
.= (f | i) . j by A3, A5, FUNCT_1:49 ; :: thesis: verum

end;

i <= (len f) + (len g) by A1, NAT_1:12;
then i <= len (f ^ g) by FINSEQ_1:22;
then len ((f ^ g) | i) = i by FINSEQ_1:59;
hence (f ^ g) | i = f | i by A2, A4, FINSEQ_2:9; :: thesis: verum