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 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 (addition (A,i,j)) . d1 = (addition A) . (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by A4, A7, FUNCT_1:12

.= 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

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 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 (addition (A,i,j)) . d1 = (addition A) . (((denaming (V,A,i)) . d1),((denaming (V,A,j)) . d1)) by A4, A7, FUNCT_1:12

.= 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