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 16
.= <*a,b*> by A1, FINSEQ_6:5 ;
hence f | 2 = <*a,b*> ; :: thesis: verum