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);

hence f * N is monotone ; :: thesis: verum

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

then
netmap ((f * N),T) is monotone
;(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;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

hence f * N is monotone ; :: thesis: verum