let p be set ; :: thesis: for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) -| p = (1,((len f) -' 1)) -cut f
let D be non empty set ; :: thesis: for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) -| p = (1,((len f) -' 1)) -cut f
let f be non empty FinSequence of D; :: thesis: for g being FinSequence of D st p .. f = len f holds
(f ^ g) -| p = (1,((len f) -' 1)) -cut f
let g be FinSequence of D; :: thesis: ( p .. f = len f implies (f ^ g) -| p = (1,((len f) -' 1)) -cut f )
assume A1: p .. f = len f ; :: thesis: (f ^ g) -| p = (1,((len f) -' 1)) -cut f
p in rng f by A1, Th4;
then A2: p .. (f ^ g) = p .. f by FINSEQ_6:6;
reconsider i = (len f) - 1 as Element of NAT by INT_1:5, NAT_1:14;
A3: (len f) -' 1 = i by NAT_1:14, XREAL_1:233;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A4: len f <= len (f ^ g) by NAT_1:11;
rng f c= rng (f ^ g) by FINSEQ_1:29;
hence (f ^ g) -| p = (f ^ g) | (Seg i) by A1, A2, Th4, FINSEQ_4:33
.= (f ^ g) | i by FINSEQ_1:def 15
.= (1,((len f) -' 1)) -cut (f ^ g) by A4, A3, Th14, NAT_D:44
.= (1,((len f) -' 1)) -cut f by MSSCYC_1:2, NAT_D:44 ;
:: thesis: verum