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

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