let V, A be set ; :: thesis: for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (multiplication (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y
let d1 be NonatomicND of V,A; :: thesis: for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (multiplication (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y
let i, j be Element of V; :: thesis: ( A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (multiplication (A,i,j)) implies for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y )
assume that
A1: A is complex-containing and
A2: i in dom d1 and
A3: j in dom d1 and
A4: d1 in dom (multiplication (A,i,j)) ; :: thesis: for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y
let x, y be Complex; :: thesis: ( x = d1 . i & y = d1 . j implies (multiplication (A,i,j)) . d1 = x * y )
assume A5: ( x = d1 . i & y = d1 . j ) ; :: thesis: (multiplication (A,i,j)) . d1 = x * y
set Di = denaming (V,A,i);
set Dj = denaming (V,A,j);
A6: d1 in dom <:(denaming (V,A,i)),(denaming (V,A,j)):> by A4, FUNCT_1:11;
then A7: <:(denaming (V,A,i)),(denaming (V,A,j)):> . d1 = [((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)] by FUNCT_3:def 7;
A8: dom <:(denaming (V,A,i)),(denaming (V,A,j)):> = (dom (denaming (V,A,i))) /\ (dom (denaming (V,A,j))) by FUNCT_3:def 7;
then d1 in dom (denaming (V,A,i)) by A6, XBOOLE_0:def 4;
then A9: (denaming (V,A,i)) . d1 = denaming (i,d1) by NOMIN_1:def 18
.= d1 . i by A2, NOMIN_1:def 12 ;
d1 in dom (denaming (V,A,j)) by A6, A8, XBOOLE_0:def 4;
then A10: (denaming (V,A,j)) . d1 = denaming (j,d1) by NOMIN_1:def 18
.= d1 . j by A3, NOMIN_1:def 12 ;
A11: ( x in COMPLEX & y in COMPLEX ) by XCMPLX_0:def 2;
thus (multiplication (A,i,j)) . d1 = (multiplication A) . (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by A4, A7, FUNCT_1:12
.= multiplication (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by A1, A5, A9, A10, A11, Def6
.= x * y by A5, A9, A10, Def4 ; :: thesis: verum