let D be set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y
for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y
for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )
let F be FinSequence of Y; :: thesis: for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )
let m1, m2, k1, k2 be Nat; :: thesis: ( 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) implies ( m1 = m2 & k1 = k2 ) )
assume that
A1: ( 1 <= m1 & 1 <= m2 ) and
A2: m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) and
A3: m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) and
A4: m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) ; :: thesis: ( m1 = m2 & k1 = k2 )
set n = m1 + (Sum (Length (F | k1)));
A5: now :: thesis: not k1 <> k2
assume A6: k1 <> k2 ; :: thesis: contradiction
per cases ( k1 < k2 or k1 > k2 ) by A6, XXREAL_0:1;
suppose k1 < k2 ; :: thesis: contradiction
then k1 + 1 <= k2 by NAT_1:13;
then Sum (Length (F | (k1 + 1))) <= Sum (Length (F | k2)) by Th5;
then m1 + (Sum (Length (F | k1))) <= Sum (Length (F | k2)) by A3, XXREAL_0:2;
hence contradiction by A2, A1, NAT_1:19; :: thesis: verum
end;
suppose k1 > k2 ; :: thesis: contradiction
then k2 + 1 <= k1 by NAT_1:13;
then Sum (Length (F | (k2 + 1))) <= Sum (Length (F | k1)) by Th5;
then m1 + (Sum (Length (F | k1))) <= Sum (Length (F | k1)) by A2, A4, XXREAL_0:2;
hence contradiction by A1, NAT_1:19; :: thesis: verum
end;
end;
end;
now :: thesis: ( m1 <> m2 implies k1 <> k2 )
assume m1 <> m2 ; :: thesis: k1 <> k2
then (Sum (Length (F | k1))) - (Sum (Length (F | k2))) <> 0 by A2;
hence k1 <> k2 ; :: thesis: verum
end;
hence ( m1 = m2 & k1 = k2 ) by A5; :: thesis: verum