let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f holds

rng f = (rng (f -: p)) \/ (rng (f :- p))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

rng f = (rng (f -: p)) \/ (rng (f :- p))

let f be FinSequence of D; :: thesis: ( p in rng f implies rng f = (rng (f -: p)) \/ (rng (f :- p)) )

assume A1: p in rng f ; :: thesis: rng f = (rng (f -: p)) \/ (rng (f :- p))

then f -: p = (f -| p) ^ <*p*> by Th40;

then A2: rng (f -: p) = (rng (f -| p)) \/ (rng <*p*>) by FINSEQ_1:31;

f :- p = <*p*> ^ (f |-- p) by A1, Th41;

then A3: rng (f :- p) = (rng <*p*>) \/ (rng (f |-- p)) by FINSEQ_1:31;

f = ((f -| p) ^ <*p*>) ^ (f |-- p) by A1, FINSEQ_4:51;

hence rng f = (rng ((f -| p) ^ <*p*>)) \/ (rng (f |-- p)) by FINSEQ_1:31

.= ((rng (f -| p)) \/ ((rng <*p*>) \/ (rng <*p*>))) \/ (rng (f |-- p)) by FINSEQ_1:31

.= (((rng (f -| p)) \/ (rng <*p*>)) \/ (rng <*p*>)) \/ (rng (f |-- p)) by XBOOLE_1:4

.= (rng (f -: p)) \/ (rng (f :- p)) by A2, A3, XBOOLE_1:4 ;

:: thesis: verum

for f being FinSequence of D st p in rng f holds

rng f = (rng (f -: p)) \/ (rng (f :- p))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

rng f = (rng (f -: p)) \/ (rng (f :- p))

let f be FinSequence of D; :: thesis: ( p in rng f implies rng f = (rng (f -: p)) \/ (rng (f :- p)) )

assume A1: p in rng f ; :: thesis: rng f = (rng (f -: p)) \/ (rng (f :- p))

then f -: p = (f -| p) ^ <*p*> by Th40;

then A2: rng (f -: p) = (rng (f -| p)) \/ (rng <*p*>) by FINSEQ_1:31;

f :- p = <*p*> ^ (f |-- p) by A1, Th41;

then A3: rng (f :- p) = (rng <*p*>) \/ (rng (f |-- p)) by FINSEQ_1:31;

f = ((f -| p) ^ <*p*>) ^ (f |-- p) by A1, FINSEQ_4:51;

hence rng f = (rng ((f -| p) ^ <*p*>)) \/ (rng (f |-- p)) by FINSEQ_1:31

.= ((rng (f -| p)) \/ ((rng <*p*>) \/ (rng <*p*>))) \/ (rng (f |-- p)) by FINSEQ_1:31

.= (((rng (f -| p)) \/ (rng <*p*>)) \/ (rng <*p*>)) \/ (rng (f |-- p)) by XBOOLE_1:4

.= (rng (f -: p)) \/ (rng (f :- p)) by A2, A3, XBOOLE_1:4 ;

:: thesis: verum