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:71
.= (0. K) * (mlt p1,(0* K,n)) by FVSUM_1:83
.= n |-> (0. K) by FVSUM_1:71 ; :: thesis: verum