let x, y1, y2 be FinSequence of COMPLEX ; :: thesis: ( len x = len y1 & len y1 = len y2 implies |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)| )
assume that
A1: len x = len y1 and
A2: len y1 = len y2 ; :: thesis: |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|
A3: ( len (Re y1) = len y1 & len (Re y2) = len y2 ) by Th40;
A4: len (Im x) = len x by Th40;
A5: ( len (Im y1) = len y1 & len (Im y2) = len y2 ) by Th40;
A6: len (Re x) = len x by Th40;
|(x,(y1 - y2))| = ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),(Im (y1 - y2)))| by A2, Th43
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th43
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th43
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th43
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A1, A2, A3, A6, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A5, A4, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A6, A5, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * (|((Im x),(Re y1))| - |((Im x),(Re y2))|))) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A3, A4, RVSUM_1:124
.= |(x,y1)| - |(x,y2)| ;
hence |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)| ; :: thesis: verum