let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds () . (( . [a,f]),( . [a,g])) = . [a,(() . (f,g))]

let f, g be Element of Funcs (A,COMPLEX); :: thesis: for a being Complex holds () . (( . [a,f]),( . [a,g])) = . [a,(() . (f,g))]
let a be Complex; :: thesis: () . (( . [a,f]),( . [a,g])) = . [a,(() . (f,g))]
reconsider a = a as Element of COMPLEX by XCMPLX_0:def 2;
now :: thesis: for x being Element of A holds (() . (( . [a,f]),( . [a,g]))) . x = ( . [a,(() . (f,g))]) . x
let x be Element of A; :: thesis: (() . (( . [a,f]),( . [a,g]))) . x = ( . [a,(() . (f,g))]) . x
thus (() . (( . [a,f]),( . [a,g]))) . x = (( . [a,f]) . x) + (( . [a,g]) . x) by Th1
.= (a * (f . x)) + (( . [a,g]) . x) by Th4
.= (a * (f . x)) + (a * (g . x)) by Th4
.= a * ((f . x) + (g . x))
.= a * ((() . (f,g)) . x) by Th1
.= ( . [a,(() . (f,g))]) . x by Th4 ; :: thesis: verum
end;
hence (ComplexFuncAdd A) . (( . [a,f]),( . [a,g])) = . [a,(() . (f,g))] by FUNCT_2:63; :: thesis: verum