{ n where n is Nat : ( n in dom f & f . n <> Mean f ) } c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : ( n in dom f & f . n <> Mean f ) } or x in dom f )
assume x in { n where n is Nat : ( n in dom f & f . n <> Mean 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

end;

hence HetSet f is finite ; :: thesis: verum