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 n < 1 ; :: thesis: 1,n -cut p = 1,n -cut (p ^ q)

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

end;

suppose A2: 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

len (p ^ q) = (len p) + (len q) by FINSEQ_1:35;
then A3: n <= len (p ^ q) by A1, NAT_1:12;
then A4: ( (len (1,n -cut p)) + 1 = n + 1 & (len (1,n -cut (p ^ q))) + 1 = n + 1 ) by A1, A2, GRAPH_2:def 1;
hence len (1,n -cut p) = len (1,n -cut (p ^ q)) ; :: 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 A5: ( 1 <= k & k <= len (1,n -cut p) ) ; :: thesis: (1,n -cut p) . k = (1,n -cut (p ^ q)) . k
0 + 1 = 1 ;
then consider i being Element of NAT such that
A6: ( 0 <= i & i < len (1,n -cut p) & k = i + 1 ) by A5, GRAPH_2:1;
k <= len p by A1, A4, A5, XXREAL_0:2;
then A7: k in dom p by A5, FINSEQ_3:27;
thus (1,n -cut p) . k = p . k by A1, A2, A6, GRAPH_2:def 1
.= (p ^ q) . k by A7, FINSEQ_1:def 7
.= (1,n -cut (p ^ q)) . k by A2, A3, A4, A6, GRAPH_2:def 1 ; :: thesis: verum

end;

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

end;

end;