set f = <:f1,f2:>;
for x, y being Element of P st x <= y holds
for a, b being Element of [:Q1,Q2:] st a = <:f1,f2:> . x & b = <:f1,f2:> . y holds
a <= b
proof
let x,
y be
Element of
P;
( x <= y implies for a, b being Element of [:Q1,Q2:] st a = <:f1,f2:> . x & b = <:f1,f2:> . y holds
a <= b )
assume B1:
x <= y
;
for a, b being Element of [:Q1,Q2:] st a = <:f1,f2:> . x & b = <:f1,f2:> . y holds
a <= b
let a,
b be
Element of
[:Q1,Q2:];
( a = <:f1,f2:> . x & b = <:f1,f2:> . y implies a <= b )
assume B2:
(
a = <:f1,f2:> . x &
b = <:f1,f2:> . y )
;
a <= b
dom <:f1,f2:> = the
carrier of
P
by FUNCT_2:def 1;
then B3:
(
a = [(f1 . x),(f2 . x)] &
b = [(f1 . y),(f2 . y)] )
by FUNCT_3:def 7, B2;
(
f1 . x <= f1 . y &
f2 . x <= f2 . y )
by B1, ORDERS_3:def 5;
hence
a <= b
by YELLOW_3:11, B3;
verum
end;
hence
for b1 being Function of P,[:Q1,Q2:] st b1 = <:f1,f2:> holds
b1 is monotone
; verum