let a, b, c be set ; :: thesis: for D being non empty set

for f being FinSequence of D st f = <*a,b,c*> holds

f | 1 = <*a*>

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds

f | 1 = <*a*>

let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies f | 1 = <*a*> )

assume A1: f = <*a,b,c*> ; :: thesis: f | 1 = <*a*>

f | 1 = f | (Seg 1) by FINSEQ_1:def 15

.= <*a*> by A1, FINSEQ_6:4 ;

hence f | 1 = <*a*> ; :: thesis: verum

for f being FinSequence of D st f = <*a,b,c*> holds

f | 1 = <*a*>

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds

f | 1 = <*a*>

let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies f | 1 = <*a*> )

assume A1: f = <*a,b,c*> ; :: thesis: f | 1 = <*a*>

f | 1 = f | (Seg 1) by FINSEQ_1:def 15

.= <*a*> by A1, FINSEQ_6:4 ;

hence f | 1 = <*a*> ; :: thesis: verum