let f be real-valued FinSequence; :: thesis: ( Het f = 0 implies f is homogeneous )
assume A1: Het f = 0 ; :: thesis: f is homogeneous
set X = { n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;
assume a4: f is heterogeneous ; :: thesis: contradiction
A5: for n being Nat st n in dom f holds
f . n = Mean f
proof
let n be Nat; :: thesis: ( n in dom f implies f . n = Mean f )
assume A2: n in dom f ; :: thesis: f . n = Mean f
f . n = Mean f
proof
assume f . n <> Mean f ; :: thesis: contradiction
then n in { n where n is Nat : ( n in dom f & f . n <> Mean f ) } by A2;
hence contradiction by A1; :: thesis: verum
end;
hence f . n = Mean f ; :: thesis: verum
end;
for x, y being object st x in dom f & y in dom f holds
f . x = f . y
proof
let x, y be object ; :: thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume B1: ( x in dom f & y in dom f ) ; :: thesis: f . x = f . y
then reconsider xx = x, yy = y as Nat ;
f . xx = Mean f by A5, B1;
hence f . x = f . y by A5, B1; :: thesis: verum
end;
hence contradiction by a4; :: thesis: verum