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:86;
|(y,x)| *' = (Sum (mlt y,(x *' ))) *' by A1, Th40
.= Sum ((mlt y,(x *' )) *' ) by A1, A3, A4, Th24
.= Sum (mlt x,(y *' )) by A1, Th25
.= |(x,y)| by A1, Th40 ;
hence |(x,y)| = |(y,x)| *' ; :: thesis: verum