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, Th41
.= ((|((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, Th41
.= ((|((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, Th41
.= ((|((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, Th41
.= (((|((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:120
.= (((|((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:120
.= (((|((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:120
.= (((|((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:120
.= |(x,y1)| + |(x,y2)| ;
hence |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| ; :: thesis: verum