let i be Nat; :: 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:44
.= multreal [;] (0,R) by A1, RELAT_1:79
.= i |-> 0 by Th16, Th22, BINOP_2:2, FINSEQOP:80 ; :: thesis: verum