let D be non empty set ; :: thesis: for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds
(f ^' g) -: (g /. 1) = f
let f, g be non empty FinSequence of D; :: thesis: ( (g /. 1) .. f = len f implies (f ^' g) -: (g /. 1) = f )
assume A1: (g /. 1) .. f = len f ; :: thesis: (f ^' g) -: (g /. 1) = f
A3: g /. 1 in rng f by A1, Th4;
A5: 1 <= len f by NAT_1:14;
g /. 1 in rng f by A1, Th4;
then A6: g /. 1 = f . (len f) by A1, FINSEQ_4:29;
A7: ((len f) -' 1) + 1 = len f by NAT_1:14, XREAL_1:237;
A8: f ^' g = f ^ (2,(len g) -cut g) by GRAPH_2:def 2;
then rng f c= rng (f ^' g) by FINSEQ_1:42;
hence (f ^' g) -: (g /. 1) = ((f ^' g) -| (g /. 1)) ^ <*(g /. 1)*> by A3, FINSEQ_6:44
.= (1,((len f) -' 1) -cut f) ^ <*(g /. 1)*> by A1, A8, Th15
.= (1,((len f) -' 1) -cut f) ^ ((len f),(len f) -cut f) by A5, A6, GRAPH_2:6
.= f by A7, GRAPH_2:9, NAT_D:44 ;
:: thesis: verum