let G be Graph; :: thesis: for p being Path of G
for m being Element of NAT st m + 1 in dom p holds
( len (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = len p & rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = rng p & (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1) )
let p be Path of G; :: thesis: for m being Element of NAT st m + 1 in dom p holds
( len (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = len p & rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = rng p & (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1) )
let m be Element of NAT ; :: thesis: ( m + 1 in dom p implies ( len (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = len p & rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = rng p & (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1) ) )
set r2 = (m + 1),(len p) -cut p;
set r1 = 1,m -cut p;
set r = ((m + 1),(len p) -cut p) ^ (1,m -cut p);
set n = m + 1;
assume A1: m + 1 in dom p ; :: thesis: ( len (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = len p & rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = rng p & (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1) )
then A2: m + 1 <= len p by FINSEQ_3:27;
then A3: m + 1 < (len p) + 1 by NAT_1:13;
m <= m + 1 by NAT_1:11;
then A4: p = (1,m -cut p) ^ ((m + 1),(len p) -cut p) by A2, GRAPH_2:9, XXREAL_0:2;
thus len (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = (len (1,m -cut p)) + (len ((m + 1),(len p) -cut p)) by FINSEQ_1:35
.= len p by A4, FINSEQ_1:35 ; :: thesis: ( rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = rng p & (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1) )
thus rng (((m + 1),(len p) -cut p) ^ (1,m -cut p)) = (rng (1,m -cut p)) \/ (rng ((m + 1),(len p) -cut p)) by FINSEQ_1:44
.= rng p by A4, FINSEQ_1:44 ; :: thesis: (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = p . (m + 1)
A5: 1 <= m + 1 by A1, FINSEQ_3:27;
then (len ((m + 1),(len p) -cut p)) + (m + 1) = (len p) + 1 by A2, GRAPH_2:def 1;
then 1 + (m + 1) <= (len ((m + 1),(len p) -cut p)) + (m + 1) by A3, NAT_1:13;
then A6: 1 <= len ((m + 1),(len p) -cut p) by XREAL_1:8;
then 1 in dom ((m + 1),(len p) -cut p) by FINSEQ_3:27;
hence (((m + 1),(len p) -cut p) ^ (1,m -cut p)) . 1 = ((m + 1),(len p) -cut p) . (0 + 1) by FINSEQ_1:def 7
.= p . ((m + 1) + 0 ) by A5, A2, A6, GRAPH_2:def 1
.= p . (m + 1) ;
:: thesis: verum