deffunc H₁( Element of V) -> Element of the carrier of K = (f . $1) + (g . $1);
consider F being Function of the carrier of V, the carrier of K such that
A1: for x being Element of V holds F . x = H₁(x) from FUNCT_2:sch 4();
reconsider F = F as Functional of V ;
take F ; :: thesis: for x being Element of V holds F . x = (f . x) + (g . x)
thus for x being Element of V holds F . x = (f . x) + (g . x) by A1; :: thesis: verum