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

let j be Nat; :: thesis: ( j in dom ((f ^' g) | i) implies ((f ^' g) | i) . j = (f | i) . j )
A6: j in NAT by ORDINAL1:def 12;
assume A7: j in dom ((f ^' g) | i) ; :: thesis: ((f ^' g) | i) . j = (f | i) . j
then A8: 1 <= j by A5, FINSEQ_1:1;
j <= i by A5, A7, FINSEQ_1:1;
then A9: j <= len f by A1, XXREAL_0:2;
thus ((f ^' g) | i) . j = ((f ^' g) | (Seg i)) . j by FINSEQ_1:def 15
.= (f ^' g) . j by A5, A7, FUNCT_1:49
.= f . j by A6, A8, A9, GRAPH_2:14
.= (f | (Seg i)) . j by A5, A7, FUNCT_1:49
.= (f | i) . j by FINSEQ_1:def 15 ; :: 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 GRAPH_2:55; :: thesis: verum

end;

end;