let i be Element of NAT ; :: thesis: for K being non empty multMagma
for a, a' being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a' = p . i holds
(a * p) . i = a * a'
let K be non empty multMagma ; :: thesis: for a, a' being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a' = p . i holds
(a * p) . i = a * a'
let a, a' be Element of K; :: thesis: for p being FinSequence of the carrier of K st i in dom (a * p) & a' = p . i holds
(a * p) . i = a * a'
let p be FinSequence of the carrier of K; :: thesis: ( i in dom (a * p) & a' = p . i implies (a * p) . i = a * a' )
assume that
A1: i in dom (a * p) and
A2: a' = p . i ; :: thesis: (a * p) . i = a * a'
A3: a' in dom (the multF of K [;] a,(id the carrier of K)) by A1, A2, FUNCT_1:21;
thus (a * p) . i = (the multF of K [;] a,(id the carrier of K)) . a' by A1, A2, FUNCT_1:22
.= the multF of K . a,((id the carrier of K) . a') by A3, FUNCOP_1:42
.= a * a' by FUNCT_1:35 ; :: thesis: verum