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) = g
let f, g be non empty FinSequence of D; :: thesis: ( (g /. 1) .. f = len f implies (f ^' g) :- (g /. 1) = g )
assume A1: (g /. 1) .. f = len f ; :: thesis: (f ^' g) :- (g /. 1) = g
A2: g /. 1 in rng f by A1, Th4;
A3: 1 <= len g by NAT_1:14;
A4: 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) = <*(g /. 1)*> ^ ((f ^' g) |-- (g /. 1)) by A2, FINSEQ_6:45
.= <*(g /. 1)*> ^ (2,(len g) -cut g) by A1, A4, Th5
.= <*(g . 1)*> ^ (2,(len g) -cut g) by A3, FINSEQ_4:24
.= (1,1 -cut g) ^ ((1 + 1),(len g) -cut g) by A3, GRAPH_2:6
.= g by GRAPH_2:9, NAT_1:14 ;
:: thesis: verum