let R be Ring; :: thesis: for X being set
for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,(0_Funcs (X,R))) = f
let X be set ; :: thesis: for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,(0_Funcs (X,R))) = f
let f be Element of Funcs (X, the carrier of R); :: thesis: (ADD (X,R)) . (f,(0_Funcs (X,R))) = f
set F1 = (ADD (X,R)) . (f,(0_Funcs (X,R)));
B1: ( dom ((ADD (X,R)) . (f,(0_Funcs (X,R)))) = X & dom f = X ) by FUNCT_2:def 1;
for x being object st x in X holds
((ADD (X,R)) . (f,(0_Funcs (X,R)))) . x = f . x

proof

let x be object ; :: thesis: ( x in X implies ((ADD (X,R)) . (f,(0_Funcs (X,R)))) . x = f . x )
assume A0: x in X ; :: thesis: ((ADD (X,R)) . (f,(0_Funcs (X,R)))) . x = f . x
then reconsider fx = f . x, y = (X --> (0. R)) . x as Element of R by FUNCT_2:5;
((ADD (X,R)) . (f,(0_Funcs (X,R)))) . x = fx + y by A0, Th1
.= fx + (0. R) by A0, FUNCOP_1:7 ;
hence ((ADD (X,R)) . (f,(0_Funcs (X,R)))) . x = f . x ; :: thesis: verum

end;

hence (ADD (X,R)) . (f,(0_Funcs (X,R))) = f by B1; :: thesis: verum