let r, s, t be real number ; :: thesis: ( r <= s & 0 <= t implies r * t <= s * t )
reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;
assume that
A1: r <= s and
A2: 0 <= t ; :: thesis: r * t <= s * t
not o in [:{0 },REAL+ :] by ARYTM_0:5, XBOOLE_0:3;
then A3: t in REAL+ by A2, XXREAL_0:def 5;
for x' being Element of REAL
for r being real number st x' = r holds
* x',z1 = r * t

proof

let x' be Element of REAL ; :: thesis: for r being real number st x' = r holds
* x',z1 = r * t
let r be real number ; :: thesis: ( x' = r implies * x',z1 = r * t )
assume A4: x' = r ; :: thesis: * x',z1 = r * t
consider x1, x2, y1, y2 being Element of REAL such that
A5: r = [*x1,x2*] and
A6: t = [*y1,y2*] and
A7: r * t = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by XCMPLX_0:def 5;
x2 = 0 by A5, Lm1;
then A8: * x2,y1 = 0 by ARYTM_0:14;
A9: y2 = 0 by A6, Lm1;
then * x1,y2 = 0 by ARYTM_0:14;
then A10: + (* x1,y2),(* x2,y1) = 0 by A8, ARYTM_0:13;
( r = x1 & t = y1 ) by A5, A6, Lm1;
hence * x',z1 = + (* x1,y1),(* (opp x2),y2) by A4, A9, ARYTM_0:13, ARYTM_0:14
.= + (* x1,y1),(opp (* x2,y2)) by ARYTM_0:17
.= r * t by A7, A10, ARYTM_0:def 7 ;
:: thesis: verum

end;

then A11: ( * y1,z1 = s * t & * x1,z1 = r * t ) ;
assume A12: not r * t <= s * t ; :: thesis: contradiction
then A13: t <> 0 ;

per cases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0 },REAL+ :] & s in REAL+ ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] ) ) by A1, XXREAL_0:def 5;

suppose that A14: r in REAL+ and
A15: s in REAL+ ; :: thesis: contradiction

consider s', t'' being Element of REAL+ such that
A16: s = s' and
A17: ( t = t'' & * y1,z1 = s' *' t'' ) by A3, A15, ARYTM_0:def 3;
consider x', t' being Element of REAL+ such that
A18: r = x' and
A19: ( t = t' & * x1,z1 = x' *' t' ) by A3, A14, ARYTM_0:def 3;
ex x'', s'' being Element of REAL+ st
( r = x'' & s = s'' & x'' <=' s'' ) by A1, A14, A15, XXREAL_0:def 5;
then x' *' t' <=' s' *' t' by A18, A16, ARYTM_1:8;
hence contradiction by A11, A12, A19, A17, Lm2; :: thesis: verum

end;

suppose that A20: r in [:{0 },REAL+ :] and
A21: s in REAL+ ; :: thesis: contradiction

ex x', t' being Element of REAL+ st
( r = [0 ,x'] & t = t' & * x1,z1 = [0 ,(t' *' x')] ) by A3, A13, A20, ARYTM_0:def 3;
then * x1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
then A22: not * x1,z1 in REAL+ by ARYTM_0:5, XBOOLE_0:3;
ex s', t'' being Element of REAL+ st
( s = s' & t = t'' & * y1,z1 = s' *' t'' ) by A3, A21, ARYTM_0:def 3;
then not * y1,z1 in [:{0 },REAL+ :] by ARYTM_0:5, XBOOLE_0:3;
hence contradiction by A11, A12, A22, XXREAL_0:def 5; :: thesis: verum

end;

suppose that A23: r in [:{0 },REAL+ :] and
A24: s in [:{0 },REAL+ :] ; :: thesis: contradiction

consider s', t'' being Element of REAL+ such that
A25: s = [0 ,s'] and
A26: t = t'' and
A27: * y1,z1 = [0 ,(t'' *' s')] by A3, A13, A24, ARYTM_0:def 3;
A28: * y1,z1 in [:{0 },REAL+ :] by A27, Lm3, ZFMISC_1:106;
consider x'', s'' being Element of REAL+ such that
A29: r = [0 ,x''] and
A30: s = [0 ,s''] and
A31: s'' <=' x'' by A1, A23, A24, XXREAL_0:def 5;
A32: s' = s'' by A30, A25, ZFMISC_1:33;
consider x', t' being Element of REAL+ such that
A33: r = [0 ,x'] and
A34: t = t' and
A35: * x1,z1 = [0 ,(t' *' x')] by A3, A13, A23, ARYTM_0:def 3;
A36: * x1,z1 in [:{0 },REAL+ :] by A35, Lm3, ZFMISC_1:106;
x' = x'' by A29, A33, ZFMISC_1:33;
then s' *' t' <=' x' *' t' by A31, A32, ARYTM_1:8;
hence contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2; :: thesis: verum

end;

end;