deffunc H1( Element of F2()) -> Element of F1() = F3(( the mapping of F2() . $1));
A1:
for i being Element of F2() holds H1(i) in the carrier of F1()
;
consider f being Function of the carrier of F2(), the carrier of F1() such that
A2:
for i being Element of F2() holds f . i = H1(i)
from FUNCT_2:sch 8(A1);
set M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #);
( RelStr(# the carrier of NetStr(# the carrier of F2(), the InternalRel of F2(),f #), the InternalRel of NetStr(# the carrier of F2(), the InternalRel of F2(),f #) #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & [#] F2() is directed )
by WAYBEL_0:def 6;
then
[#] NetStr(# the carrier of F2(), the InternalRel of F2(),f #) is directed
by WAYBEL_0:3;
then reconsider M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #) as prenet of F1() by WAYBEL_0:def 6;
take
M
; ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) )
thus
( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) )
by A2; verum