let a, b, c be real number ; :: thesis: ( a <= b & 0 <= c implies a * c <= b * c )
assume that
A1: a <= b and
A2: 0 <= c ; :: thesis: a * c <= b * c
not o 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 b', c'' being Element of REAL+ such that
A10: b = b' and
A11: c = c'' and
A12: * y1,z1 = b' *' c'' by A3, A9, ARYTM_0:def 3;
consider a', c' being Element of REAL+ such that
A13: a = a' and
A14: c = c' and
A15: * x1,z1 = a' *' c' by A3, A8, ARYTM_0:def 3;
ex a'', b'' being Element of REAL+ st
( a = a'' & b = b'' & a'' <=' b'' ) by A1, A8, A9, XXREAL_0:def 5;
then a' *' c' <=' b' *' c' 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 a', c' being Element of REAL+ st
( a = [0 ,a'] & c = c' & * x1,z1 = [0 ,(c' *' a')] ) by A3, A7, A16, ARYTM_0:def 3;
then * x1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
then A18: not * x1,z1 in REAL+ by ARYTM_0:5, XBOOLE_0:3;
ex b', c'' being Element of REAL+ st
( b = b' & c = c'' & * y1,z1 = b' *' c'' ) by A3, A17, ARYTM_0:def 3;
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 b', c'' being Element of REAL+ such that
A21: b = [0 ,b'] and
A22: c = c'' and
A23: * y1,z1 = [0 ,(c'' *' b')] by A3, A7, A20, ARYTM_0:def 3;
A24: * y1,z1 in [:{0 },REAL+ :] by A23, Lm4, ZFMISC_1:106;
consider a'', b'' being Element of REAL+ such that
A25: a = [0 ,a''] and
A26: b = [0 ,b''] and
A27: b'' <=' a'' by A1, A19, A20, XXREAL_0:def 5;
A28: b' = b'' by A26, A21, ZFMISC_1:33;
consider a', c' being Element of REAL+ such that
A29: a = [0 ,a'] and
A30: c = c' and
A31: * x1,z1 = [0 ,(c' *' a')] by A3, A7, A19, ARYTM_0:def 3;
A32: * x1,z1 in [:{0 },REAL+ :] by A31, Lm4, ZFMISC_1:106;
a' = a'' by A25, A29, ZFMISC_1:33;
then b' *' c' <=' a' *' c' by A27, A28, ARYTM_1:8;
hence contradiction by A4, A5, A6, A30, A31, A22, A23, A32, A24, Lm1; :: thesis: verum

end;

end;