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 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 ; :: thesis: ( 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; :: thesis: verum