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 by XREAL_0:def 1;
A1: Im x19 = 0 by COMPLEX1:def 2;
A2: Im x29 = 0 by COMPLEX1:def 2;
A3: Im y29 = 0 by COMPLEX1:def 2;
A4: Im y19 = 0 by COMPLEX1:def 2;
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:32
.= ((x19 *') + (y29 *')) + ((<i> * (y19 - x29)) *') by COMPLEX1:32
.= (x19 + (y29 *')) + ((<i> * (y19 - x29)) *') by A1, COMPLEX1:38
.= (x19 + y29) + ((<i> * (y19 - x29)) *') by A3, COMPLEX1:38
.= (x19 + y29) + ((- <i>) * ((y19 - x29) *')) by COMPLEX1:31, COMPLEX1:35
.= (x19 + y29) + ((- <i>) * ((y19 *') - (x29 *'))) by COMPLEX1:34
.= (x19 + y29) + ((- <i>) * (y19 - (x29 *'))) by A4, COMPLEX1:38
.= (x19 + y29) + ((- <i>) * (y19 - x29)) by A2, COMPLEX1:38
.= |(x,y)| ;
hence |(x,y)| = |(y,x)| *' ; :: thesis: verum