per cases
( A is empty or not A is empty )
;

end;

suppose A1:
A is empty
; :: thesis: ex b_{1} being Function of D,REAL st

for X being Element of D st X in D holds

b_{1} . X = Sum (f * (canFS (eqSupport (f,X))))

for X being Element of D st X in D holds

b

set F = the Function of D,REAL;

take the Function of D,REAL ; :: thesis: for X being Element of D st X in D holds

the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X))))

let X be Element of D; :: thesis: ( X in D implies the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X)))) )

assume X in D ; :: thesis: the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X))))

hence the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X)))) by A1; :: thesis: verum

end;take the Function of D,REAL ; :: thesis: for X being Element of D st X in D holds

the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X))))

let X be Element of D; :: thesis: ( X in D implies the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X)))) )

assume X in D ; :: thesis: the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X))))

hence the Function of D,REAL . X = Sum (f * (canFS (eqSupport (f,X)))) by A1; :: thesis: verum

suppose
not A is empty
; :: thesis: ex b_{1} being Function of D,REAL st

for X being Element of D st X in D holds

b_{1} . X = Sum (f * (canFS (eqSupport (f,X))))

for X being Element of D st X in D holds

b

then reconsider B = A as non empty set ;

reconsider f = f as finite-support Function of B,REAL ;

reconsider E = D as a_partition of B ;

defpred S_{1}[ object , object ] means ex Y being Element of E st

( $1 = Y & $2 = Sum (f * (canFS (eqSupport (f,Y)))) );

A2: for X being object st X in E holds

ex y being object st

( y in REAL & S_{1}[X,y] )

A3: for X being object st X in E holds

S_{1}[X,F . X]
from FUNCT_2:sch 1(A2);

reconsider F = F as Function of D,REAL ;

take F ; :: thesis: for X being Element of D st X in D holds

F . X = Sum (f * (canFS (eqSupport (f,X))))

for X being Element of E st X in E holds

F . X = Sum (f * (canFS (eqSupport (f,X))))

F . X = Sum (f * (canFS (eqSupport (f,X)))) ; :: thesis: verum

end;reconsider f = f as finite-support Function of B,REAL ;

reconsider E = D as a_partition of B ;

defpred S

( $1 = Y & $2 = Sum (f * (canFS (eqSupport (f,Y)))) );

A2: for X being object st X in E holds

ex y being object st

( y in REAL & S

proof

consider F being Function of E,REAL such that
let X be object ; :: thesis: ( X in E implies ex y being object st

( y in REAL & S_{1}[X,y] ) )

assume X in E ; :: thesis: ex y being object st

( y in REAL & S_{1}[X,y] )

then reconsider x = X as Element of E ;

set y = Sum (f * (canFS (eqSupport (f,x))));

take Sum (f * (canFS (eqSupport (f,x)))) ; :: thesis: ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S_{1}[X, Sum (f * (canFS (eqSupport (f,x))))] )

thus ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S_{1}[X, Sum (f * (canFS (eqSupport (f,x))))] )
by XREAL_0:def 1; :: thesis: verum

end;( y in REAL & S

assume X in E ; :: thesis: ex y being object st

( y in REAL & S

then reconsider x = X as Element of E ;

set y = Sum (f * (canFS (eqSupport (f,x))));

take Sum (f * (canFS (eqSupport (f,x)))) ; :: thesis: ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S

thus ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S

A3: for X being object st X in E holds

S

reconsider F = F as Function of D,REAL ;

take F ; :: thesis: for X being Element of D st X in D holds

F . X = Sum (f * (canFS (eqSupport (f,X))))

for X being Element of E st X in E holds

F . X = Sum (f * (canFS (eqSupport (f,X))))

proof

hence
for X being Element of D st X in D holds
let X be Element of E; :: thesis: ( X in E implies F . X = Sum (f * (canFS (eqSupport (f,X)))) )

assume X in E ; :: thesis: F . X = Sum (f * (canFS (eqSupport (f,X))))

consider Y being Element of E such that

A4: X = Y and

A5: F . X = Sum (f * (canFS (eqSupport (f,Y)))) by A3;

thus F . X = Sum (f * (canFS (eqSupport (f,X)))) by A4, A5; :: thesis: verum

end;assume X in E ; :: thesis: F . X = Sum (f * (canFS (eqSupport (f,X))))

consider Y being Element of E such that

A4: X = Y and

A5: F . X = Sum (f * (canFS (eqSupport (f,Y)))) by A3;

thus F . X = Sum (f * (canFS (eqSupport (f,X)))) by A4, A5; :: thesis: verum

F . X = Sum (f * (canFS (eqSupport (f,X)))) ; :: thesis: verum