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

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