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:86;
len (x *' ) = len x by COMPLSP2:def 1;
then |((x *' ),(y *' ))| = Sum (mlt (x *' ),((y *' ) *' )) by A1, A4, Th40
.= Sum ((mlt x,(y *' )) *' ) by A1, A4, Th28
.= (Sum (mlt x,(y *' ))) *' by A3, A5, Th24
.= |(x,y)| *' by A1, Th40 ;
hence |(x,y)| *' = |((x *' ),(y *' ))| ; :: thesis: verum