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 #);
NetStr(# the carrier of F2(),the InternalRel of F2(),f #) is directed
proof
A3:
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() #)
;
A4:
[#] F2() is
directed
by WAYBEL_0:def 6;
thus
[#] NetStr(# the
carrier of
F2(),the
InternalRel of
F2(),
f #) is
directed
by A3, A4, WAYBEL_0:3;
:: according to WAYBEL_0:def 6 :: thesis: verum
end;
then reconsider M = NetStr(# the carrier of F2(),the InternalRel of F2(),f #) as prenet of F1() ;
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