let A be Preorder; :: thesis: for X being Element of (QuotientOrder A)
for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)
let X be Element of (QuotientOrder A); :: thesis: for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)
let f be Function of the carrier of A,REAL; :: thesis: eqSupport (f,X) = eqSupport ((- f),X)
consider D being a_partition of the carrier of A, Y being Element of D such that
D = the carrier of (QuotientOrder A) and
A1: X = Y and
A2: eqSupport (f,X) = eqSupport (f,Y) by Def12;
thus eqSupport (f,X) = eqSupport ((- f),Y) by A2, Th52
.= eqSupport ((- f),X) by A1 ; :: thesis: verum