let i be Nat; :: thesis: for K being non empty multMagma
for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let K be non empty multMagma ; :: thesis: for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let a, a9 be Element of K; :: thesis: for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let p be FinSequence of the carrier of K; :: thesis: ( i in dom (a * p) & a9 = p . i implies (a * p) . i = a * a9 )
assume A1: ( i in dom (a * p) & a9 = p . i ) ; :: thesis: (a * p) . i = a * a9
then A2: a9 in dom ( the multF of K [;] (a,(id the carrier of K))) by FUNCT_1:11;
thus (a * p) . i = ( the multF of K [;] (a,(id the carrier of K))) . a9 by A1, FUNCT_1:12
.= the multF of K . (a,((id the carrier of K) . a9)) by A2, FUNCOP_1:32
.= a * a9 ; :: thesis: verum