let G be Graph; :: thesis: for p being Path of G
for m being 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 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 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:25;
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, FINSEQ_6:135, 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:22
.= len p by A4, FINSEQ_1:22 ; :: 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:31
.= rng p by A4, FINSEQ_1:31 ; :: thesis: ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) . 1 = p . (m + 1)
A5: 1 <= m + 1 by A1, FINSEQ_3:25;
then (len (((m + 1),(len p)) -cut p)) + (m + 1) = (len p) + 1 by A2, FINSEQ_6:def 4;
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:6;
then 1 in dom (((m + 1),(len p)) -cut p) by FINSEQ_3:25;
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, FINSEQ_6:def 4
.= p . (m + 1) ;
:: thesis: verum