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; :: thesis: ( 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 ; :: thesis: 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:]; :: thesis: ( a = <:f1,f2:> . x & b = <:f1,f2:> . y implies a <= b )
assume B2: ( a = <:f1,f2:> . x & b = <:f1,f2:> . y ) ; :: thesis: 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; :: thesis: verum

end;

hence for b₁ being Function of P,[:Q1,Q2:] st b₁ = <:f1,f2:> holds
b₁ is monotone ; :: thesis: verum