let n be Element of 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 )
assume A1: len f <= n ; :: thesis: f | n = f
A2: ( dom f = Seg (len f) & f | n = f | (Seg n) ) by FINSEQ_1:def 3, FINSEQ_1:def 15;
then dom f c= Seg n by A1, FINSEQ_1:7;
hence f | n = f by A2, RELAT_1:97; :: thesis: verum