let S, T be up-complete LATTICE; for f being Function of S,T
for N being non empty monotone NetStr over S st f is monotone holds
f * N is monotone
let f be Function of S,T; for N being non empty monotone NetStr over S st f is monotone holds
f * N is monotone
let N be non empty monotone NetStr over S; ( f is monotone implies f * N is monotone )
assume A1:
f is monotone
; f * N is monotone
A2:
netmap (N,S) is monotone
by WAYBEL_0:def 9;
A3:
netmap ((f * N),T) = f * (netmap (N,S))
by WAYBEL_9:def 8;
set g = netmap ((f * N),T);
now for x, y being Element of (f * N) st x <= y holds
(netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . ylet x,
y be
Element of
(f * N);
( x <= y implies (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y )assume A4:
x <= y
;
(netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . yA5:
RelStr(# the
carrier of
N, the
InternalRel of
N #)
= RelStr(# the
carrier of
(f * N), the
InternalRel of
(f * N) #)
by WAYBEL_9:def 8;
then reconsider x9 =
x,
y9 =
y as
Element of
N ;
A6:
dom (netmap (N,S)) = the
carrier of
(f * N)
by A5, FUNCT_2:def 1;
then A7:
(netmap ((f * N),T)) . x = f . ((netmap (N,S)) . x)
by A3, FUNCT_1:13;
A8:
(netmap ((f * N),T)) . y = f . ((netmap (N,S)) . y)
by A3, A6, FUNCT_1:13;
[x,y] in the
InternalRel of
(f * N)
by A4, ORDERS_2:def 5;
then
x9 <= y9
by A5, ORDERS_2:def 5;
then
(netmap (N,S)) . x9 <= (netmap (N,S)) . y9
by A2;
hence
(netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y
by A1, A7, A8;
verum end;
then
netmap ((f * N),T) is monotone
;
hence
f * N is monotone
; verum