let f be real-valued FinSequence; :: thesis: for i, j being Nat st i in dom f & j in dom f & i <> j & f . i <> Mean f & f . j <> Mean f holds
Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))))
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j & f . i <> Mean f & f . j <> Mean f implies Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) )
assume A0: ( i in dom f & j in dom f & i <> j ) ; :: thesis: ( not f . i <> Mean f or not f . j <> Mean f or Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) )
assume FF: ( f . i <> Mean f & f . j <> Mean f ) ; :: thesis: Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))))
set g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)));
zz: f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent by ReplaceGamma, A0;
set a = Mean f;
set b = ((f . i) + (f . j)) - (Mean f);
FX: HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) <> HetSet f
proof
assume h2: HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) = HetSet f ; :: thesis: contradiction
not i in { n1 where n1 is Nat : ( n1 in dom (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) & (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) . n1 <> Mean (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) ) }
proof
assume i in { n1 where n1 is Nat : ( n1 in dom (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) & (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) . n1 <> Mean (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) ) } ; :: thesis: contradiction
then consider n2 being Nat such that
G1: ( n2 = i & n2 in dom (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) & (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) . n2 <> Mean (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) ) ;
thus contradiction by zz, ReplaceValue3, A0, G1; :: thesis: verum
end;
hence contradiction by h2, FF, A0; :: thesis: verum
end;
HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) c= HetSet f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) or x in HetSet f )
assume x in HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) ; :: thesis: x in HetSet f
then consider n1 being Nat such that
A1: ( n1 = x & n1 in dom (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) & (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) . n1 <> Mean (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) ) ;
A2: n1 in dom f by A1, DinoDom;
f . n1 <> Mean f
proof
per cases ( n1 = i or n1 = j or ( n1 <> i & n1 <> j ) ) ;
suppose n1 = j ; :: thesis: f . n1 <> Mean f
hence f . n1 <> Mean f by FF; :: thesis: verum
end;
suppose B1: ( n1 <> i & n1 <> j ) ; :: thesis: f . n1 <> Mean f
f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent by ReplaceGamma, A0;
hence f . n1 <> Mean f by B1, ReplaceValue, A0, A2, A1; :: thesis: verum
end;
end;
end;
hence x in HetSet f by A1, A2; :: thesis: verum
end;
then HetSet (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) c< HetSet f by FX;
hence Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f)))) by CARD_2:48; :: thesis: verum