let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |(x,y)| = |(y,x)| *' )
assume len x = len y ; :: thesis: |(x,y)| = |(y,x)| *'
set x1 = |((Re y),(Re x))|;
set x2 = |((Re y),(Im x))|;
set y1 = |((Im y),(Re x))|;
set y2 = |((Im y),(Im x))|;
reconsider x1' = |((Re y),(Re x))|, x2' = |((Re y),(Im x))|, y1' = |((Im y),(Re x))|, y2' = |((Im y),(Im x))| as Element of REAL ;
A1: Im x1' = 0 by COMPLEX1:def 3;
A2: Im x2' = 0 by COMPLEX1:def 3;
A3: Im y1' = 0 by COMPLEX1:def 3;
A4: Im y2' = 0 by COMPLEX1:def 3;
reconsider x1' = |((Re y),(Re x))|, x2' = |((Re y),(Im x))|, y1' = |((Im y),(Re x))|, y2' = |((Im y),(Im x))| as Element of COMPLEX by XCMPLX_0:def 2;
|(y,x)| *' = ((x1' + y2') + (<i> * (y1' - x2'))) *'
.= ((x1' + y2') *' ) + ((<i> * (y1' - x2')) *' ) by COMPLEX1:118
.= ((x1' *' ) + (y2' *' )) + ((<i> * (y1' - x2')) *' ) by COMPLEX1:118
.= (x1' + (y2' *' )) + ((<i> * (y1' - x2')) *' ) by A1, COMPLEX1:124
.= (x1' + y2') + ((<i> * (y1' - x2')) *' ) by A4, COMPLEX1:124
.= (x1' + y2') + ((- <i> ) * ((y1' - x2') *' )) by COMPLEX1:116, COMPLEX1:121
.= (x1' + y2') + ((- <i> ) * ((y1' *' ) - (x2' *' ))) by COMPLEX1:120
.= (x1' + y2') + ((- <i> ) * (y1' - (x2' *' ))) by A3, COMPLEX1:124
.= (x1' + y2') + ((- <i> ) * (y1' - x2')) by A2, COMPLEX1:124
.= |(x,y)| ;
hence |(x,y)| = |(y,x)| *' ; :: thesis: verum