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 x' = x as Element of n -tuples_on REAL ;
(0 * x) + x = (0 * x') + (1 * x') by RVSUM_1:74
.= (0 + 1) * x' by RVSUM_1:72
.= x by RVSUM_1:74 ;
hence ( (0 * x) + x = x & x + (0* n) = x ) by RVSUM_1:33; :: thesis: verum