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:80;

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

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

then len g <> 0 ;
then len g > 0 ;
then len g >= 0 + 1 by NAT_1:13;
then i + 1 <= (len f) + (len g) by A1, XREAL_1:9;
then i + 1 <= (len (f ^' g)) + 1 by A3, GRAPH_2:13;
then i <= len (f ^' g) by XREAL_1:8;
then A4: len ((f ^' g) | i) = i by FINSEQ_1:80;
then X: 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 )
A5: j in NAT by ORDINAL1:def 13;
assume A6: j in dom ((f ^' g) | i) ; :: thesis: ((f ^' g) | i) . j = (f | i) . j
then j <= i by X, FINSEQ_1:3;
then A7: ( 1 <= j & j <= len f ) by A1, A6, X, FINSEQ_1:3, XXREAL_0:2;
thus ((f ^' g) | i) . j = ((f ^' g) | (Seg i)) . j by FINSEQ_1:def 15
.= (f ^' g) . j by A6, X, FUNCT_1:72
.= f . j by A5, A7, GRAPH_2:14
.= (f | (Seg i)) . j by A6, X, FUNCT_1:72
.= (f | i) . j by FINSEQ_1:def 15 ; :: thesis: verum

end;

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

end;

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

hence (f ^' g) | i = f | i by GRAPH_2:59; :: thesis: verum

end;

end;