let n be Nat; for x being Element of REAL n holds
( 1 * x = x & 0 * x = 0* n )
let x be Element of REAL n; ( 1 * x = x & 0 * x = 0* n )
reconsider x' = x as Element of n -tuples_on REAL ;
0 * x =
((0 * x') + x') - x'
by RVSUM_1:63
.=
x' - x'
by Th1
.=
0* n
by RVSUM_1:58
;
hence
( 1 * x = x & 0 * x = 0* n )
by RVSUM_1:74; verum