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