let n be Nat; :: thesis: for D being set
for f being FinSequence of D st len f <= n holds
f | n = f
let D be 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
hence f | n = f by A1, FINSEQ_1:5, RELAT_1:68; :: thesis: verum