let n be Nat; :: thesis: for x being Element of REAL n holds
( (0 * x) + x = x & x + (0* n) = x )
let x be Element of REAL n; :: thesis: ( (0 * x) + x = x & x + (0* n) = x )
reconsider x9 = x as Element of n -tuples_on REAL ;
(0 * x) + x = (0 * x9) + (1 * x9) by RVSUM_1:52
.= (0 + 1) * x9 by RVSUM_1:50
.= x by RVSUM_1:52 ;
hence ( (0 * x) + x = x & x + (0* n) = x ) by RVSUM_1:16; :: thesis: verum