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 that
A1: f <> {} and
A2: f /. 1 = p ; :: thesis: ( f -: p = <*p*> & f :- p = f )
A3: p in rng f by A1, A2, Th42;
p .. f = 1 by A1, A2, Th43;
then A4: f -| p = {} by A3, FINSEQ_4:40;
hence f -: p = {} ^ <*p*> by A3, Th40
.= <*p*> by FINSEQ_1:34 ;
:: thesis: f :- p = f
thus f = ({} ^ <*p*>) ^ (f |-- p) by A3, A4, FINSEQ_4:51
.= <*p*> ^ (f |-- p) by FINSEQ_1:34
.= f :- p by A3, Th41 ; :: thesis: verum