let i, j be Element of (f * N); :: according to WAYBEL21:def 2 :: thesis: ( i <= j implies (f * N) . i >= (f * N) . j )
A1: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def 8;
A2: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def 8;
then reconsider x = i, y = j as Element of N ;
assume i <= j ; :: thesis: (f * N) . i >= (f * N) . j
then x <= y by A2, YELLOW_0:1;
then N . x >= N . y by Def2;
then f . (N . x) >= f . (N . y) by WAYBEL_1:def 2;
then (f * N) . i >= f . (N . y) by A1, FUNCT_2:15;
hence (f * N) . i >= (f * N) . j by A1, FUNCT_2:15; :: thesis: verum