let n be Element of NAT ; :: thesis: for D being set
for f being FinSequence of D st n >= len f holds
len (f | n) = len f
let D be set ; :: thesis: for f being FinSequence of D st n >= len f holds
len (f | n) = len f
let f be FinSequence of D; :: 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