deffunc H_{1}( Element of V1) -> Element of the carrier of V2 = (f1 . $1) + (f2 . $1);

consider F being Function of V1,V2 such that

A1: for v being Element of V1 holds F . v = H_{1}(v)
from FUNCT_2:sch 4();

reconsider F = F as Function of V1,V2 ;

take F ; :: thesis: for v being Element of V1 holds F . v = (f1 . v) + (f2 . v)

thus for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) by A1; :: thesis: verum

consider F being Function of V1,V2 such that

A1: for v being Element of V1 holds F . v = H

reconsider F = F as Function of V1,V2 ;

take F ; :: thesis: for v being Element of V1 holds F . v = (f1 . v) + (f2 . v)

thus for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) by A1; :: thesis: verum