let A be FinSequence; :: thesis: for a being set st #occurrences (a,A) = len A holds
max# A = len A
let a be set ; :: thesis: ( #occurrences (a,A) = len A implies max# A = len A )
assume #occurrences (a,A) = len A ; :: thesis: max# A = len A
then ( len A <= max# A & max# A <= len A ) by Def23, Th56;
hence max# A = len A by XXREAL_0:1; :: thesis: verum