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

( (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