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 A2: f = ((f -| p) ^ <*p*>) ^ (f |-- p) by FINSEQ_4:66;
f -: p = (f -| p) ^ <*p*> by A1, Th44;
then A3: rng (f -: p) = (rng (f -| p)) \/ (rng <*p*>) by FINSEQ_1:44;
f :- p = <*p*> ^ (f |-- p) by A1, Th45;
then A4: rng (f :- p) = (rng <*p*>) \/ (rng (f |-- p)) by FINSEQ_1:44;
thus rng f = (rng ((f -| p) ^ <*p*>)) \/ (rng (f |-- p)) by A2, FINSEQ_1:44
.= ((rng (f -| p)) \/ ((rng <*p*>) \/ (rng <*p*>))) \/ (rng (f |-- p)) by FINSEQ_1:44
.= (((rng (f -| p)) \/ (rng <*p*>)) \/ (rng <*p*>)) \/ (rng (f |-- p)) by XBOOLE_1:4
.= (rng (f -: p)) \/ (rng (f :- p)) by A3, A4, XBOOLE_1:4 ; :: thesis: verum