let X be non empty set ; for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
let Y be RealLinearSpace; for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
let f, g be Element of Funcs (X, the carrier of Y); (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
hence
(FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
by FUNCT_2:63; verum