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