let n be Nat; :: thesis: for D being set
for f being b₁ -valued FinSequence st n >= len f holds
len (f | n) = len f
let D be set ; :: thesis: for f being D -valued FinSequence st n >= len f holds
len (f | n) = len f
let f be D -valued FinSequence; :: thesis: ( n >= len f implies len (f | n) = len f )
assume n >= len f ; :: thesis: len (f | n) = len f
then reconsider k = n - (len f) as Element of NAT by NAT_1:21;
len (f | n) = len (f | ((len f) + k)) ;
hence len (f | n) = len f ; :: thesis: verum