let i be natural Number ; :: thesis: for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0
let R be Element of i -tuples_on REAL; :: thesis: 0 * R = i |-> 0
A1: rng R c= REAL ;
thus 0 * R = multreal [;] (0,((id REAL) * R)) by FUNCOP_1:34
.= multreal [;] (0,R) by A1, RELAT_1:53
.= i |-> 0 by Th3, Th8, BINOP_2:2, FINSEQOP:76 ; :: thesis: verum