let x1, x2 be FinSequence of COMPLEX ; :: thesis: ( len x1 = len x2 implies (x1 + x2) *' = (x1 *' ) + (x2 *' ) )
assume A1: len x1 = len x2 ; :: thesis: (x1 + x2) *' = (x1 *' ) + (x2 *' )
then A2: len (x1 + x2) = len x1 by Th6;
reconsider x' = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y' = x2 as Element of (len x2) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider x3 = x1 *' as Element of (len (x1 *' )) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider x4 = x2 *' as Element of (len (x2 *' )) -tuples_on COMPLEX by FINSEQ_2:110;
A3: len x1 = len (x1 *' ) by Def1;
A4: len x2 = len (x2 *' ) by Def1;
then len ((x1 *' ) + (x2 *' )) = len x1 by A1, A3, Th6;
then A5: len ((x1 + x2) *' ) = len ((x1 *' ) + (x2 *' )) by A2, Def1;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len ((x1 + x2) *' ) implies ((x1 + x2) *' ) . i = (x3 + x4) . i )
A6: i in NAT by ORDINAL1:def 13;
assume ( 1 <= i & i <= len ((x1 + x2) *' ) ) ; :: thesis: ((x1 + x2) *' ) . i = (x3 + x4) . i
then A7: ( 1 <= i & i <= len (x1 + x2) ) by Def1;
hence ((x1 + x2) *' ) . i = ((x1 + x2) . i) *' by Def1
.= ((x' . i) + (y' . i)) *' by A1, A6, Th18
.= ((x1 . i) *' ) + ((x2 . i) *' ) by COMPLEX1:118
.= ((x1 *' ) . i) + ((x2 . i) *' ) by A2, A7, Def1
.= ((x1 *' ) . i) + ((x2 *' ) . i) by A1, A2, A7, Def1
.= (x3 + x4) . i by A1, A3, A4, A6, Th18 ;
:: thesis: verum

end;

hence (x1 + x2) *' = (x1 *' ) + (x2 *' ) by A5, FINSEQ_1:18; :: thesis: verum