let D be set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y
for k1, k2 being Nat st k1 <= k2 holds
Sum (Length (F | k1)) <= Sum (Length (F | k2))
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y
for k1, k2 being Nat st k1 <= k2 holds
Sum (Length (F | k1)) <= Sum (Length (F | k2))
let F be FinSequence of Y; :: thesis: for k1, k2 being Nat st k1 <= k2 holds
Sum (Length (F | k1)) <= Sum (Length (F | k2))
let k1, k2 be Nat; :: thesis: ( k1 <= k2 implies Sum (Length (F | k1)) <= Sum (Length (F | k2)) )
assume k1 <= k2 ; :: thesis: Sum (Length (F | k1)) <= Sum (Length (F | k2))
then (F | k2) | k1 = F | k1 by FINSEQ_1:82;
then F | k2 = (F | k1) ^ ((F | k2) /^ k1) by RFINSEQ8;
then Length (F | k2) = (Length (F | k1)) ^ (Length ((F | k2) /^ k1)) by Th4;
then Sum (Length (F | k2)) = (Sum (Length (F | k1))) + (Sum (Length ((F | k2) /^ k1))) by RVSUM_1:75;
hence Sum (Length (F | k1)) <= Sum (Length (F | k2)) by NAT_1:11; :: thesis: verum