let C be set ; :: thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let D1, D2 be non empty complex-membered set ; :: thesis: for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let f1 be Function of C,D1; :: thesis: for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let f2 be Function of C,D2; :: thesis: for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
A1: dom (f1 + f2) = C by FUNCT_2:def 1;
let c be Element of C; :: thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)

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

suppose not C is empty ; :: thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)

hence (f1 + f2) . c = (f1 . c) + (f2 . c) by A1, Def1; :: thesis: verum

end;

suppose A2: C is empty ; :: thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)

then f1 . c = 0 ;
hence (f1 + f2) . c = (f1 . c) + (f2 . c) by A2; :: thesis: verum

end;

end;