let n be Nat; :: thesis: for x being Element of REAL n holds

( 1 * x = x & 0 * x = 0* n )

let x be Element of REAL n; :: thesis: ( 1 * x = x & 0 * x = 0* n )

reconsider x9 = x as Element of n -tuples_on REAL ;

0 * x = ((0 * x9) + x9) - x9 by RVSUM_1:42

.= x9 - x9 by Th1

.= 0* n by RVSUM_1:37 ;

hence ( 1 * x = x & 0 * x = 0* n ) by RVSUM_1:52; :: thesis: verum

( 1 * x = x & 0 * x = 0* n )

let x be Element of REAL n; :: thesis: ( 1 * x = x & 0 * x = 0* n )

reconsider x9 = x as Element of n -tuples_on REAL ;

0 * x = ((0 * x9) + x9) - x9 by RVSUM_1:42

.= x9 - x9 by Th1

.= 0* n by RVSUM_1:37 ;

hence ( 1 * x = x & 0 * x = 0* n ) by RVSUM_1:52; :: thesis: verum