let p be set ; 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 ; 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; 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; ( p .. f = len f implies (f ^ g) -| p = (1,((len f) -' 1)) -cut f )
assume A1:
p .. f = len f
; (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
;
verum