per cases ( A is empty or not A is empty ) ;
suppose A1: A is empty ; :: thesis: ex b1 being Function of D,REAL st
for X being Element of D st X in D holds
b1 . X = Sum (f * (canFS (eqSupport (f,X))))

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;
suppose not A is empty ; :: thesis: ex b1 being Function of D,REAL st
for X being Element of D st X in D holds
b1 . X = Sum (f * (canFS (eqSupport (f,X))))

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 S1[ 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 & S1[X,y] )
proof
let X be object ; :: thesis: ( X in E implies ex y being object st
( y in REAL & S1[X,y] ) )

assume X in E ; :: thesis: ex y being object st
( y in REAL & S1[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 & S1[X, Sum (f * (canFS (eqSupport (f,x))))] )
thus ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S1[X, Sum (f * (canFS (eqSupport (f,x))))] ) by XREAL_0:def 1; :: thesis: verum
end;
consider F being Function of E,REAL such that
A3: for X being object st X in E holds
S1[X,F . X] from 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
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;
hence for X being Element of D st X in D holds
F . X = Sum (f * (canFS (eqSupport (f,X)))) ; :: thesis: verum
end;
end;