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 | 2 = <*a,b*>

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

f | 2 = <*a,b*>

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

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

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

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

hence f | 2 = <*a,b*> ; :: thesis: verum

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

f | 2 = <*a,b*>

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

f | 2 = <*a,b*>

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

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

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

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

hence f | 2 = <*a,b*> ; :: thesis: verum