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 A1, FINSEQ_2:92;

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 Th7;

(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 A1, FINSEQ_2:92;

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 Th7;

per cases
( not i in Seg (len x) or i in Seg (len x) )
;

end;

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 A2, A4, FINSEQ_2:124;

not i in dom y29 by A3, A4, FINSEQ_2:124;

then (x2 - y2) . i = 0 - 0 by FUNCT_1:def 2

.= (x2 . i) - 0 by A5, FUNCT_1:def 2

.= (x2 . i) - (y2 . i) by A6, FUNCT_1:def 2 ;

hence (x - y) . i = (x . i) - (y . i) ; :: thesis: verum

end;A6: not i in dom y2 by A2, A4, FINSEQ_2:124;

not i in dom y29 by A3, A4, FINSEQ_2:124;

then (x2 - y2) . i = 0 - 0 by FUNCT_1:def 2

.= (x2 . i) - 0 by A5, FUNCT_1:def 2

.= (x2 . i) - (y2 . i) by A6, FUNCT_1:def 2 ;

hence (x - y) . i = (x . i) - (y . i) ; :: thesis: verum