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