let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds p .. (f :- p) = 1
let p be Element of D; :: thesis: for f being FinSequence of D holds p .. (f :- p) = 1
let f be FinSequence of D; :: thesis: p .. (f :- p) = 1
(f :- p) /. 1 = p by FINSEQ_5:53;
hence p .. (f :- p) = 1 by Th43; :: thesis: verum