let R be Ring; :: thesis: for X being set
for v1, w1 being Element of Funcs (X, the carrier of R)
for v, w being Element of (FS_Funcs (X,R)) st v1 = v & w1 = w holds
v + w = (ADD (X,R)) . (v1,w1)
let X be set ; :: thesis: for v1, w1 being Element of Funcs (X, the carrier of R)
for v, w being Element of (FS_Funcs (X,R)) st v1 = v & w1 = w holds
v + w = (ADD (X,R)) . (v1,w1)
let v1, w1 be Element of Funcs (X, the carrier of R); :: thesis: for v, w being Element of (FS_Funcs (X,R)) st v1 = v & w1 = w holds
v + w = (ADD (X,R)) . (v1,w1)
let v, w be Element of (FS_Funcs (X,R)); :: thesis: ( v1 = v & w1 = w implies v + w = (ADD (X,R)) . (v1,w1) )
set V1 = fs_Funcs (X,R);
assume A1: ( v1 = v & w1 = w ) ; :: thesis: v + w = (ADD (X,R)) . (v1,w1)
[v,w] in [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):] ;
then [v,w] in dom ((ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):]) by FUNCT_2:def 1;
hence v + w = (ADD (X,R)) . (v1,w1) by A1, FUNCT_1:47; :: thesis: verum