let V, A be set ; 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; 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; ( 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))
; 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; ( x = d1 . i & y = d1 . j implies (multiplication (A,i,j)) . d1 = x * y )
assume A5:
( x = d1 . i & y = d1 . j )
; (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
; verum