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
(f -: p) ^ ((f :- p) /^ 1) = f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
(f -: p) ^ ((f :- p) /^ 1) = f
let f be FinSequence of D; :: thesis: ( p in rng f implies (f -: p) ^ ((f :- p) /^ 1) = f )
assume A1: p in rng f ; :: thesis: (f -: p) ^ ((f :- p) /^ 1) = f
then A2: rng (f |-- p) c= rng f by FINSEQ_4:59;
rng f c= D by FINSEQ_1:def 4;
then rng (f |-- p) c= D by A2, XBOOLE_1:1;
then reconsider f1 = f |-- p as FinSequence of D by FINSEQ_1:def 4;
thus (f -: p) ^ ((f :- p) /^ 1) = ((f -| p) ^ <*p*>) ^ ((f :- p) /^ 1) by A1, Th44
.= ((f -| p) ^ <*p*>) ^ ((<*p*> ^ f1) /^ 1) by A1, Th45
.= ((f -| p) ^ <*p*>) ^ (f |-- p) by Th49
.= f by A1, FINSEQ_4:66 ; :: thesis: verum