let n be Nat; :: thesis: for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n

let v be Element of n -tuples_on REAL; :: thesis: mlt (v,(0* n)) = 0* n

len (0* n) = n by CARD_1:def 7;

then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:92;

A1: len (0* n) = n by CARD_1:def 7;

A2: for j being Nat st j in dom (0* n) holds

(mlt (v,(0* n))) . j = (0* n) . j

then dom (mlt (v,(0* n))) = dom (0* n) by A1, FINSEQ_3:29;

hence mlt (v,(0* n)) = 0* n by A2, FINSEQ_1:13; :: thesis: verum

let v be Element of n -tuples_on REAL; :: thesis: mlt (v,(0* n)) = 0* n

len (0* n) = n by CARD_1:def 7;

then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:92;

A1: len (0* n) = n by CARD_1:def 7;

A2: for j being Nat st j in dom (0* n) holds

(mlt (v,(0* n))) . j = (0* n) . j

proof

len (mlt (v,z)) = n
by CARD_1:def 7;
let j be Nat; :: thesis: ( j in dom (0* n) implies (mlt (v,(0* n))) . j = (0* n) . j )

assume j in dom (0* n) ; :: thesis: (mlt (v,(0* n))) . j = (0* n) . j

thus (mlt (v,(0* n))) . j = 0 by Th1

.= (n |-> 0) . j

.= (0* n) . j by EUCLID:def 4 ; :: thesis: verum

end;assume j in dom (0* n) ; :: thesis: (mlt (v,(0* n))) . j = (0* n) . j

thus (mlt (v,(0* n))) . j = 0 by Th1

.= (n |-> 0) . j

.= (0* n) . j by EUCLID:def 4 ; :: thesis: verum

then dom (mlt (v,(0* n))) = dom (0* n) by A1, FINSEQ_3:29;

hence mlt (v,(0* n)) = 0* n by A2, FINSEQ_1:13; :: thesis: verum