let i be Element of NAT ; :: thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
(x - y) . i = (x . i) - (y . i)
let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies (x - y) . i = (x . i) - (y . i) )
reconsider x2 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y2 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y29 = x2 - y2 as Element of (len (x2 - y2)) -tuples_on COMPLEX by FINSEQ_2:110;
assume A1: len x = len y ; :: thesis: (x - y) . i = (x . i) - (y . i)
then A2: len (x - y) = len x by Th7;

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

suppose A3: not i in Seg (len x) ; :: thesis: (x - y) . i = (x . i) - (y . i)

then A4: not i in dom x2 by FINSEQ_2:144;
A5: not i in dom y2 by A1, A3, FINSEQ_2:144;
not i in dom y29 by A2, A3, FINSEQ_2:144;
then (x2 - y2) . i = 0 - 0 by FUNCT_1:def 4
.= (x2 . i) - 0 by A4, FUNCT_1:def 4
.= (x2 . i) - (y2 . i) by A5, FUNCT_1:def 4 ;
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 A2, FINSEQ_2:144;
hence (x - y) . i = (x . i) - (y . i) by VALUED_1:13; :: thesis: verum

end;

end;