let S, T be up-complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: ( f is monotone implies f * N is monotone )
assume A1: f is monotone ; :: thesis: 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 :: thesis: for x, y being Element of (f * N) st x <= y holds
(netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y

let x, y be Element of (f * N); :: thesis: ( x <= y implies (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y )
assume A4: x <= y ; :: thesis: (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y
A5: 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; :: thesis: verum

end;

then netmap ((f * N),T) is monotone ;
hence f * N is monotone ; :: thesis: verum