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