let A be set ; :: thesis: for D being a_partition of A

for X being Element of D

for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let D be a_partition of A; :: thesis: for X being Element of D

for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let X be Element of D; :: thesis: for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let f be Function of A,REAL; :: thesis: eqSupport (f,X) = eqSupport ((- f),X)

A1: rng f c= COMPLEX by NUMBERS:11;

dom f = A by FUNCT_2:def 1;

then f is Function of A,COMPLEX by FUNCT_2:2, A1;

hence eqSupport (f,X) = eqSupport ((- f),X) by Th10; :: thesis: verum

for X being Element of D

for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let D be a_partition of A; :: thesis: for X being Element of D

for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let X be Element of D; :: thesis: for f being Function of A,REAL holds eqSupport (f,X) = eqSupport ((- f),X)

let f be Function of A,REAL; :: thesis: eqSupport (f,X) = eqSupport ((- f),X)

A1: rng f c= COMPLEX by NUMBERS:11;

dom f = A by FUNCT_2:def 1;

then f is Function of A,COMPLEX by FUNCT_2:2, A1;

hence eqSupport (f,X) = eqSupport ((- f),X) by Th10; :: thesis: verum