let f be real-valued FinSequence; :: thesis: MeanLess f c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MeanLess f or x in dom f )
assume x in MeanLess 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