let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f <> {} & f /. 1 = p holds
( f -: p = <*p*> & f :- p = f )
let p be Element of D; :: thesis: for f being FinSequence of D st f <> {} & f /. 1 = p holds
( f -: p = <*p*> & f :- p = f )
let f be FinSequence of D; :: thesis: ( f <> {} & f /. 1 = p implies ( f -: p = <*p*> & f :- p = f ) )
assume A1: ( f <> {} & f /. 1 = p ) ; :: thesis: ( f -: p = <*p*> & f :- p = f )
then A2: p in rng f by Th46;
p .. f = 1 by A1, Th47;
then A3: f -| p = {} by A2, FINSEQ_4:52;
hence f -: p = {} ^ <*p*> by A2, Th44
.= <*p*> by FINSEQ_1:47 ;
:: thesis: f :- p = f
thus f = ({} ^ <*p*>) ^ (f |-- p) by A2, A3, FINSEQ_4:66
.= <*p*> ^ (f |-- p) by FINSEQ_1:47
.= f :- p by A2, Th45 ; :: thesis: verum