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

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