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
A2: g /. 1 in rng f by A1, Th4;
g /. 1 in rng f by A1, Th4;
then A3: g /. 1 = f . (len f) by A1, FINSEQ_4:19;
A4: 1 <= len f by NAT_1:14;
A5: ((len f) -' 1) + 1 = len f by NAT_1:14, XREAL_1:235;
A6: 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) = ((f ^' g) -| (g /. 1)) ^ <*(g /. 1)*> by A2, FINSEQ_6:40
.= ((1,((len f) -' 1)) -cut f) ^ <*(g /. 1)*> by A1, A6, Th15
.= ((1,((len f) -' 1)) -cut f) ^ (((len f),(len f)) -cut f) by A4, A3, FINSEQ_6:132
.= f by A5, FINSEQ_6:135, NAT_D:44 ;
:: thesis: verum