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