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 FINSEQ_6:def 5;
then rng f c= rng (f ^' g) by FINSEQ_1:29;
hence (f ^' g) :- (g /. 1) = <*(g /. 1)*> ^ ((f ^' g) |-- (g /. 1)) by A2, FINSEQ_6:41
.= <*(g /. 1)*> ^ ((2,(len g)) -cut g) by A1, A4, Th5
.= <*(g . 1)*> ^ ((2,(len g)) -cut g) by A3, FINSEQ_4:15
.= ((1,1) -cut g) ^ (((1 + 1),(len g)) -cut g) by A3, FINSEQ_6:132
.= g by FINSEQ_6:135, NAT_1:14 ;
:: thesis: verum