let D be set ; :: thesis: for f, g being FinSequence of D
for i being Nat st i <= len f holds
(f ^' g) | i = f | i
let f, g be FinSequence of D; :: thesis: for i being Nat st i <= len f holds
(f ^' g) | i = f | i
let i be Nat; :: 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;

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

suppose A3: g <> {} ; :: thesis: (f ^' g) | i = f | i

then len g >= 0 + 1 by NAT_1:13;
then i + 1 <= (len f) + (len g) by A1, XREAL_1:7;
then i + 1 <= (len (f ^' g)) + 1 by A3, FINSEQ_6:139;
then i <= len (f ^' g) by XREAL_1:6;
then A4: len ((f ^' g) | i) = i by FINSEQ_1:59;
then A5: dom ((f ^' g) | i) = Seg i by FINSEQ_1:def 3;

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

let j be Nat; :: thesis: ( j in dom ((f ^' g) | i) implies ((f ^' g) | i) . j = (f | i) . j )
assume A6: j in dom ((f ^' g) | i) ; :: thesis: ((f ^' g) | i) . j = (f | i) . j
then A7: 1 <= j by A5, FINSEQ_1:1;
j <= i by A5, A6, FINSEQ_1:1;
then A8: j <= len f by A1, XXREAL_0:2;
thus ((f ^' g) | i) . j = ((f ^' g) | (Seg i)) . j by FINSEQ_1:def 16
.= (f ^' g) . j by A5, A6, FUNCT_1:49
.= f . j by A7, A8, FINSEQ_6:140
.= (f | (Seg i)) . j by A5, A6, FUNCT_1:49
.= (f | i) . j by FINSEQ_1:def 16 ; :: thesis: verum

end;

hence (f ^' g) | i = f | i by A2, A4, FINSEQ_2:9; :: thesis: verum

end;

suppose g = {} ; :: thesis: (f ^' g) | i = f | i

hence (f ^' g) | i = f | i by FINSEQ_6:157; :: thesis: verum

end;

end;