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 )
A1: rng f c= D by FINSEQ_1:def 4;
assume A2: p in rng f ; :: thesis: (f -: p) ^ ((f :- p) /^ 1) = f
then rng (f |-- p) c= rng f by FINSEQ_4:44;
then rng (f |-- p) c= D by A1;
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 A2, Th40
.= ((f -| p) ^ <*p*>) ^ ((<*p*> ^ f1) /^ 1) by A2, Th41
.= ((f -| p) ^ <*p*>) ^ (f |-- p) by Th45
.= f by A2, FINSEQ_4:51 ; :: thesis: verum