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

suppose A1: A is empty ; :: thesis: ex b₁ being Function of D,REAL st
for X being Element of D st X in D holds
b₁ . 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 b₁ being Function of D,REAL st
for X being Element of D st X in D holds
b₁ . 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 S₁[ 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₁[X,y] )

proof

let X be object ; :: thesis: ( X in E implies ex y being object st
( y in REAL & S₁[X,y] ) )
assume X in E ; :: thesis: ex y being object st
( y in REAL & S₁[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₁[X, Sum (f * (canFS (eqSupport (f,x))))] )
thus ( Sum (f * (canFS (eqSupport (f,x)))) in REAL & S₁[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
S₁[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))))

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;