let i be Element of NAT ; :: thesis: for x, y being complex-valued FinSequence st len x = len y holds
(x + y) . i = (x . i) + (y . i)

let x, y be complex-valued FinSequence; :: thesis: ( len x = len y implies (x + y) . i = (x . i) + (y . i) )
A1: ( x is FinSequence of COMPLEX & y is FinSequence of COMPLEX ) by Lm2;
then reconsider x2 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2 = y as Element of (len y) -tuples_on COMPLEX by ;
reconsider y29 = x2 + y2 as Element of (len (x2 + y2)) -tuples_on COMPLEX by FINSEQ_2:92;
assume A2: len x = len y ; :: thesis: (x + y) . i = (x . i) + (y . i)
then A3: len (x + y) = len x by Th6;
per cases ( not i in Seg (len x) or i in Seg (len x) ) ;
suppose A4: not i in Seg (len x) ; :: thesis: (x + y) . i = (x . i) + (y . i)
then A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by ;
not i in dom y29 by ;
then (x2 + y2) . i = 0 + 0 by FUNCT_1:def 2
.= (x2 . i) + 0 by
.= (x2 . i) + (y2 . i) by ;
hence (x + y) . i = (x . i) + (y . i) ; :: thesis: verum
end;
suppose i in Seg (len x) ; :: thesis: (x + y) . i = (x . i) + (y . i)
then i in dom y29 by ;
hence (x + y) . i = (x . i) + (y . i) by VALUED_1:def 1; :: thesis: verum
end;
end;