let x, y be FinSequence of COMPLEX ; :: 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 x19 = |((Re y),(Re x))|, x29 = |((Re y),(Im x))|, y19 = |((Im y),(Re x))|, y29 = |((Im y),(Im x))| as Element of REAL ;
A1: Im x19 = 0 by COMPLEX1:def 3;
A2: Im x29 = 0 by COMPLEX1:def 3;
A3: Im y29 = 0 by COMPLEX1:def 3;
A4: Im y19 = 0 by COMPLEX1:def 3;
reconsider x19 = |((Re y),(Re x))|, x29 = |((Re y),(Im x))|, y19 = |((Im y),(Re x))|, y29 = |((Im y),(Im x))| as Element of COMPLEX by XCMPLX_0:def 2;
|(y,x)| *' = ((x19 + y29) + (<i> * (y19 - x29))) *'
.= ((x19 + y29) *' ) + ((<i> * (y19 - x29)) *' ) by COMPLEX1:118
.= ((x19 *' ) + (y29 *' )) + ((<i> * (y19 - x29)) *' ) by COMPLEX1:118
.= (x19 + (y29 *' )) + ((<i> * (y19 - x29)) *' ) by A1, COMPLEX1:124
.= (x19 + y29) + ((<i> * (y19 - x29)) *' ) by A3, COMPLEX1:124
.= (x19 + y29) + ((- <i> ) * ((y19 - x29) *' )) by COMPLEX1:116, COMPLEX1:121
.= (x19 + y29) + ((- <i> ) * ((y19 *' ) - (x29 *' ))) by COMPLEX1:120
.= (x19 + y29) + ((- <i> ) * (y19 - (x29 *' ))) by A4, COMPLEX1:124
.= (x19 + y29) + ((- <i> ) * (y19 - x29)) by A2, COMPLEX1:124
.= |(x,y)| ;
hence |(x,y)| = |(y,x)| *' ; :: thesis: verum