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 (addition (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (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 (addition (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (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 (addition (A,i,j)) implies for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (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 (addition (A,i,j)) ; :: thesis: for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (A,i,j)) . d1 = x + y

let x, y be Complex; :: thesis: ( x = d1 . i & y = d1 . j implies (addition (A,i,j)) . d1 = x + y )
assume A5: ( x = d1 . i & y = d1 . j ) ; :: thesis: (addition (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 ;
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 ;
then A9: (denaming (V,A,i)) . d1 = denaming (i,d1) by NOMIN_1:def 18
.= d1 . i by ;
d1 in dom (denaming (V,A,j)) by ;
then A10: (denaming (V,A,j)) . d1 = denaming (j,d1) by NOMIN_1:def 18
.= d1 . j by ;
A11: ( x in COMPLEX & y in COMPLEX ) by XCMPLX_0:def 2;
thus (addition (A,i,j)) . d1 = () . (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by
.= addition (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by A1, A5, A9, A10, A11, Def5
.= x + y by A5, A9, A10, Def3 ; :: thesis: verum