let n be Element of NAT ; :: thesis: for K being Field
for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K)
let K be Field; :: thesis: for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K)
let p1 be Element of n -tuples_on the carrier of K; :: thesis: mlt (p1,(n |-> (0. K))) = n |-> (0. K)
thus mlt (p1,(n |-> (0. K))) = mlt (p1,((0. K) * (0* (K,n)))) by FVSUM_1:58
.= (0. K) * (mlt (p1,(0* (K,n)))) by FVSUM_1:69
.= n |-> (0. K) by FVSUM_1:58 ; :: thesis: verum