let n be Element of NAT ; :: thesis: for p, q being FinSequence st n <= len p holds
(1,n) -cut p = (1,n) -cut (p ^ q)
let p, q be FinSequence; :: thesis: ( n <= len p implies (1,n) -cut p = (1,n) -cut (p ^ q) )
assume A1: n <= len p ; :: thesis: (1,n) -cut p = (1,n) -cut (p ^ q)

per cases ( n < 1 or 1 <= n ) ;

suppose A2: n < 1 ; :: thesis: (1,n) -cut p = (1,n) -cut (p ^ q)

then (1,n) -cut p = {} by GRAPH_2:def 1;
hence (1,n) -cut p = (1,n) -cut (p ^ q) by A2, GRAPH_2:def 1; :: thesis: verum

end;

suppose A3: 1 <= n ; :: thesis: (1,n) -cut p = (1,n) -cut (p ^ q)

set cp = (1,n) -cut p;
set cpq = (1,n) -cut (p ^ q);

now

A4: (len ((1,n) -cut p)) + 1 = n + 1 by A1, A3, GRAPH_2:def 1;
len (p ^ q) = (len p) + (len q) by FINSEQ_1:22;
then A5: n <= len (p ^ q) by A1, NAT_1:12;
then A6: (len ((1,n) -cut (p ^ q))) + 1 = n + 1 by A3, GRAPH_2:def 1;
hence len ((1,n) -cut p) = len ((1,n) -cut (p ^ q)) by A4; :: thesis: for k being Nat st 1 <= k & k <= len ((1,n) -cut p) holds
((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len ((1,n) -cut p) implies ((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k )
assume that
A7: 1 <= k and
A8: k <= len ((1,n) -cut p) ; :: thesis: ((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k
k <= len p by A1, A4, A8, XXREAL_0:2;
then A9: k in dom p by A7, FINSEQ_3:25;
0 + 1 = 1 ;
then A10: ex i being Element of NAT st
( 0 <= i & i < len ((1,n) -cut p) & k = i + 1 ) by A7, A8, GRAPH_2:1;
hence ((1,n) -cut p) . k = p . k by A1, A3, GRAPH_2:def 1
.= (p ^ q) . k by A9, FINSEQ_1:def 7
.= ((1,n) -cut (p ^ q)) . k by A3, A5, A4, A6, A10, GRAPH_2:def 1 ;
:: thesis: verum

end;

hence (1,n) -cut p = (1,n) -cut (p ^ q) by FINSEQ_1:14; :: thesis: verum

end;

end;