let f be real-valued FinSequence; :: thesis: MeanMore f c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MeanMore f or x in dom f )
assume x in MeanMore f ; :: thesis: x in dom f
then ex n being Nat st
( x = n & n in dom f & f . n > Mean f ) ;
hence x in dom f ; :: thesis: verum