let i be Nat; :: thesis: for r1, r2 being real number
for R being Element of i -tuples_on REAL holds (r1 * r2) * R = r1 * (r2 * R)
let r1, r2 be real number ; :: thesis: for R being Element of i -tuples_on REAL holds (r1 * r2) * R = r1 * (r2 * R)
let R be Element of i -tuples_on REAL ; :: thesis: (r1 * r2) * R = r1 * (r2 * R)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
thus (r1 * r2) * R = (multreal [;] (multreal . s1,s2),(id REAL )) * R by BINOP_2:def 11
.= (multreal [;] s1,(multreal [;] s2,(id REAL ))) * R by FUNCOP_1:77
.= ((multreal [;] s1,(id REAL )) * (multreal [;] s2,(id REAL ))) * R by FUNCOP_1:69
.= r1 * (r2 * R) by RELAT_1:55 ; :: thesis: verum