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