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 A1: ( len x1 = len x2 & len x2 = len y ) ; :: thesis: |((x1 + x2),y)| = |(x1,y)| + |(x2,y)|
A2: len (Re x1) = len x1 by Th48;
A3: len (Re x2) = len x2 by Th48;
A4: len (Re y) = len y by Th48;
A5: len (Im x1) = len x1 by Th48;
A6: len (Im x2) = len x2 by Th48;
A7: len (Im y) = len y by Th48;
|((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, Th49
.= ((|(((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, Th49
.= ((|(((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, Th49
.= ((|(((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, Th49
.= (((|((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, A4, EUCLID_2:19
.= (((|((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, A7, EUCLID_2:19
.= (((|((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, A4, A5, A6, EUCLID_2:19
.= (((|((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, A5, A6, A7, EUCLID_2:19
.= |(x1,y)| + |(x2,y)| ;
hence |((x1 + x2),y)| = |(x1,y)| + |(x2,y)| ; :: thesis: verum