let n be Nat; :: thesis: for D being non empty set

for f being FinSequence of D st len f <= n holds

f | n = f

let D be non empty set ; :: thesis: for f being FinSequence of D st len f <= n holds

f | n = f

let f be FinSequence of D; :: thesis: ( len f <= n implies f | n = f )

A1: dom f = Seg (len f) by FINSEQ_1:def 3;

assume len f <= n ; :: thesis: f | n = f

then ( f | n = f | (Seg n) & dom f c= Seg n ) by A1, FINSEQ_1:5, FINSEQ_1:def 15;

hence f | n = f by RELAT_1:68; :: thesis: verum

for f being FinSequence of D st len f <= n holds

f | n = f

let D be non empty set ; :: thesis: for f being FinSequence of D st len f <= n holds

f | n = f

let f be FinSequence of D; :: thesis: ( len f <= n implies f | n = f )

A1: dom f = Seg (len f) by FINSEQ_1:def 3;

assume len f <= n ; :: thesis: f | n = f

then ( f | n = f | (Seg n) & dom f c= Seg n ) by A1, FINSEQ_1:5, FINSEQ_1:def 15;

hence f | n = f by RELAT_1:68; :: thesis: verum