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