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

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