let r, s, t be Real; :: 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
0 is Element of REAL+ by ARYTM_2:20;
then not 0 in by ;
then A3: t in REAL+ by ;
for x9 being Element of REAL
for r being Real st x9 = r holds
* (x9,z1) = r * t
proof
let x9 be Element of REAL ; :: thesis: for r being Real st x9 = r holds
* (x9,z1) = r * t

let r be Real; :: thesis: ( x9 = r implies * (x9,z1) = r * t )
assume A4: x9 = r ; :: thesis: * (x9,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 ;
then A8: * (x2,y1) = 0 by ARYTM_0:12;
A9: y2 = 0 by ;
then * (x1,y2) = 0 by ARYTM_0:12;
then A10: + ((* (x1,y2)),(* (x2,y1))) = 0 by ;
( r = x1 & t = y1 ) by A5, A6, Lm1;
hence * (x9,z1) = + ((* (x1,y1)),(* ((opp x2),y2))) by
.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15
.= r * t by ;
:: 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 & s in REAL+ ) or ( r in & s in ) ) by ;
suppose that A14: r in REAL+ and
A15: s in REAL+ ; :: thesis: contradiction
consider s9, t99 being Element of REAL+ such that
A16: s = s9 and
A17: ( t = t99 & * (y1,z1) = s9 *' t99 ) by ;
consider x9, t9 being Element of REAL+ such that
A18: r = x9 and
A19: ( t = t9 & * (x1,z1) = x9 *' t9 ) by ;
ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by ;
then x9 *' t9 <=' s9 *' t9 by ;
hence contradiction by A11, A12, A19, A17, Lm2; :: thesis: verum
end;
suppose that A20: r in and
A21: s in REAL+ ; :: thesis: contradiction
ex x9, t9 being Element of REAL+ st
( r = [0,x9] & t = t9 & * (x1,z1) = [0,(t9 *' x9)] ) by ;
then * (x1,z1) in by ;
then A22: not * (x1,z1) in REAL+ by ;
ex s9, t99 being Element of REAL+ st
( s = s9 & t = t99 & * (y1,z1) = s9 *' t99 ) by ;
then not * (y1,z1) in by ;
hence contradiction by A11, A12, A22, XXREAL_0:def 5; :: thesis: verum
end;
suppose that A23: r in and
A24: s in ; :: thesis: contradiction
consider s9, t99 being Element of REAL+ such that
A25: s = [0,s9] and
A26: t = t99 and
A27: * (y1,z1) = [0,(t99 *' s9)] by ;
A28: * (y1,z1) in by ;
consider x99, s99 being Element of REAL+ such that
A29: r = [0,x99] and
A30: s = [0,s99] and
A31: s99 <=' x99 by ;
A32: s9 = s99 by ;
consider x9, t9 being Element of REAL+ such that
A33: r = [0,x9] and
A34: t = t9 and
A35: * (x1,z1) = [0,(t9 *' x9)] by ;
A36: * (x1,z1) in by ;
x9 = x99 by ;
then s9 *' t9 <=' x9 *' t9 by ;
hence contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2; :: thesis: verum
end;
end;