let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y & 0 < len y implies |(x,y)| = |(y,x)| *' )
assume that
A1: len x = len y and
A2: 0 < len y ; :: thesis: |(x,y)| = |(y,x)| *'
A3: 0 + 1 <= len x by A1, A2, NAT_1:8;
len (x *') = len x by COMPLSP2:def 1;
then A4: len (mlt (y,(x *'))) = len y by A1, FINSEQ_2:72;
|(y,x)| *' = (Sum (mlt (y,(x *')))) *' by A1, Th37
.= Sum ((mlt (y,(x *'))) *') by A1, A3, A4, Th21
.= Sum (mlt (x,(y *'))) by A1, Th22
.= |(x,y)| by A1, Th37 ;
hence |(x,y)| = |(y,x)| *' ; :: thesis: verum