let S, T be RelStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: g is monotone
reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;
let x, y be Element of K; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or g . x <= g . y )
assume A5: x <= y ; :: thesis: 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; :: thesis: verum