let x1, x2, y be FinSequence of COMPLEX ; :: thesis: ( len x1 = len x2 & len x2 = len y implies |((x1 + x2),y)| = |(x1,y)| + |(x2,y)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y ; :: thesis: |((x1 + x2),y)| = |(x1,y)| + |(x2,y)|
A3: ( len (Re x1) = len x1 & len (Re x2) = len x2 ) by Th40;
A4: len (Im y) = len y by Th40;
A5: ( len (Im x1) = len x1 & len (Im x2) = len x2 ) by Th40;
A6: len (Re y) = len y by Th40;
|((x1 + x2),y)| = ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |((Re (x1 + x2)),(Im y))|)) + (<i> * |((Im (x1 + x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th41
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |((Im (x1 + x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th41
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th41
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, Th41
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A3, A6, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A3, A4, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * (|((Im x1),(Re y))| + |((Im x2),(Re y))|))) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A6, A5, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * (|((Im x1),(Re y))| + |((Im x2),(Re y))|))) + (|((Im x1),(Im y))| + |((Im x2),(Im y))|) by A1, A2, A5, A4, RVSUM_1:120
.= |(x1,y)| + |(x2,y)| ;
hence |((x1 + x2),y)| = |(x1,y)| + |(x2,y)| ; :: thesis: verum