let i be Nat; :: thesis: for D being set
for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i
let D be set ; :: thesis: for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i
let f, g be FinSequence of D; :: 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:80;
then A3: dom (f | i) = Seg i by FINSEQ_1:def 3;

A4: now

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:3;
then A6: j <= len f by A1, XXREAL_0:2;
( j in NAT & 1 <= j ) by A3, A5, FINSEQ_1:3, ORDINAL1:def 13;
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:72
.= f . j by A7, FINSEQ_1:def 7
.= (f | i) . j by A3, A5, FUNCT_1:72 ; :: thesis: verum

end;

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