let S, T be RelStr ; for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let K, L be non empty RelStr ; for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let f be Function of S,T; for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let g be Function of K,L; ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone implies g is monotone )
assume that
A1:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #)
and
A2:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #)
and
A3:
f = g
and
A4:
f is monotone
; g is monotone
reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;
let x, y be Element of K; WAYBEL_1:def 2 ( not x <= y or g . x <= g . y )
assume A5:
x <= y
; g . x <= g . y
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1,T1 ;
x1 <= y1
by A1, A5;
then
f1 . x1 <= f1 . y1
by A4, WAYBEL_1:def 2;
hence
g . x <= g . y
by A2, A3; verum