let a, b, c be Real; :: thesis: ( a <= b & 0 <= c implies a * c <= b * c )
assume that
A1: a <= b and
A2: 0 <= c ; :: thesis: a * c <= b * c
0 is Element of REAL+ by ARYTM_2:20;
then not 0 in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
then A3: c in REAL+ by A2, XXREAL_0:def 5;
reconsider x1 = a, y1 = b, z1 = c as Element of REAL by XREAL_0:def 1;
A4: * (y1,z1) = b * c by Lm11;
A5: * (x1,z1) = a * c by Lm11;
assume A6: not a * c <= b * c ; :: thesis: contradiction
then A7: c <> 0 ;

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

suppose that A8: a in REAL+ and
A9: b in REAL+ ; :: thesis: contradiction

consider b9, c99 being Element of REAL+ such that
A10: b = b9 and
A11: c = c99 and
A12: * (y1,z1) = b9 *' c99 by A3, A9, ARYTM_0:def 2;
consider a9, c9 being Element of REAL+ such that
A13: a = a9 and
A14: c = c9 and
A15: * (x1,z1) = a9 *' c9 by A3, A8, ARYTM_0:def 2;
ex a99, b99 being Element of REAL+ st
( a = a99 & b = b99 & a99 <=' b99 ) by A1, A8, A9, XXREAL_0:def 5;
then a9 *' c9 <=' b9 *' c9 by A13, A10, ARYTM_1:8;
hence contradiction by A4, A5, A6, A14, A15, A11, A12, Lm1; :: thesis: verum

end;

suppose that A16: a in [:{0},REAL+:] and
A17: b in REAL+ ; :: thesis: contradiction

ex a9, c9 being Element of REAL+ st
( a = [0,a9] & c = c9 & * (x1,z1) = [0,(c9 *' a9)] ) by A3, A7, A16, ARYTM_0:def 2;
then * (x1,z1) in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
then A18: not * (x1,z1) in REAL+ by ARYTM_0:5, XBOOLE_0:3;
ex b9, c99 being Element of REAL+ st
( b = b9 & c = c99 & * (y1,z1) = b9 *' c99 ) by A3, A17, ARYTM_0:def 2;
then not * (y1,z1) in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
hence contradiction by A4, A5, A6, A18, XXREAL_0:def 5; :: thesis: verum

end;

suppose that A19: a in [:{0},REAL+:] and
A20: b in [:{0},REAL+:] ; :: thesis: contradiction

consider b9, c99 being Element of REAL+ such that
A21: b = [0,b9] and
A22: c = c99 and
A23: * (y1,z1) = [0,(c99 *' b9)] by A3, A7, A20, ARYTM_0:def 2;
A24: * (y1,z1) in [:{0},REAL+:] by A23, Lm4, ZFMISC_1:87;
consider a99, b99 being Element of REAL+ such that
A25: a = [0,a99] and
A26: b = [0,b99] and
A27: b99 <=' a99 by A1, A19, A20, XXREAL_0:def 5;
A28: b9 = b99 by A26, A21, XTUPLE_0:1;
consider a9, c9 being Element of REAL+ such that
A29: a = [0,a9] and
A30: c = c9 and
A31: * (x1,z1) = [0,(c9 *' a9)] by A3, A7, A19, ARYTM_0:def 2;
A32: * (x1,z1) in [:{0},REAL+:] by A31, Lm4, ZFMISC_1:87;
a9 = a99 by A25, A29, XTUPLE_0:1;
then b9 *' c9 <=' a9 *' c9 by A27, A28, ARYTM_1:8;
hence contradiction by A4, A5, A6, A30, A31, A22, A23, A32, A24, Lm1; :: thesis: verum

end;

end;