deffunc H_{1}( Element of F_{2}()) -> Element of F_{1}() = F_{3}(( the mapping of F_{2}() . $1));

A1: for i being Element of F_{2}() holds H_{1}(i) in the carrier of F_{1}()
;

consider f being Function of the carrier of F_{2}(), the carrier of F_{1}() such that

A2: for i being Element of F_{2}() holds f . i = H_{1}(i)
from FUNCT_2:sch 8(A1);

set M = NetStr(# the carrier of F_{2}(), the InternalRel of F_{2}(),f #);

( RelStr(# the carrier of NetStr(# the carrier of F_{2}(), the InternalRel of F_{2}(),f #), the InternalRel of NetStr(# the carrier of F_{2}(), the InternalRel of F_{2}(),f #) #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) & [#] F_{2}() is directed )
by WAYBEL_0:def 6;

then [#] NetStr(# the carrier of F_{2}(), the InternalRel of F_{2}(),f #) is directed
by WAYBEL_0:3;

then reconsider M = NetStr(# the carrier of F_{2}(), the InternalRel of F_{2}(),f #) as prenet of F_{1}() by WAYBEL_0:def 6;

take M ; :: thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) & ( for i being Element of M holds the mapping of M . i = F_{3}(( the mapping of F_{2}() . i)) ) )

thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) & ( for i being Element of M holds the mapping of M . i = F_{3}(( the mapping of F_{2}() . i)) ) )
by A2; :: thesis: verum

A1: for i being Element of F

consider f being Function of the carrier of F

A2: for i being Element of F

set M = NetStr(# the carrier of F

( RelStr(# the carrier of NetStr(# the carrier of F

then [#] NetStr(# the carrier of F

then reconsider M = NetStr(# the carrier of F

take M ; :: thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F

thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F