let S, T be up-complete LATTICE; :: thesis: for f being Function of S,T
for N being non empty monotone NetStr of 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 of S st f is monotone holds
f * N is monotone
let N be non empty monotone NetStr of 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

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:23;
A8: (netmap (f * N),T) . y = f . ((netmap N,S) . y) by A3, A6, FUNCT_1:23;
[x,y] in the InternalRel of (f * N) by A4, ORDERS_2:def 9;
then x9 <= y9 by A5, ORDERS_2:def 9;
then (netmap N,S) . x9 <= (netmap N,S) . y9 by A2, WAYBEL_1:def 2;
hence (netmap (f * N),T) . x <= (netmap (f * N),T) . y by A1, A7, A8, WAYBEL_1:def 2; :: thesis: verum

end;

then netmap (f * N),T is monotone by WAYBEL_1:def 2;
hence f * N is monotone by WAYBEL_0:def 9; :: thesis: verum