let L be non empty addLoopStr ; :: thesis: for x1, x2 being FinSequence of L
for i being Nat st len x1 = len x2 & 1 <= i & i <= len x1 holds
( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )
let x1, x2 be FinSequence of L; :: thesis: for i being Nat st len x1 = len x2 & 1 <= i & i <= len x1 holds
( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )
let i be Nat; :: thesis: ( len x1 = len x2 & 1 <= i & i <= len x1 implies ( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) ) )
assume that
A1: len x1 = len x2 and
A2: ( 1 <= i & i <= len x1 ) ; :: thesis: ( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )
reconsider x10 = x1, x20 = x2 as Element of (len x1) -tuples_on the carrier of L by A1, Th1;
A3: ( x10 /. i = x10 . i & x20 /. i = x20 . i ) by A1, A2, FINSEQ_4:15;
i in Seg (len x1) by A2, FINSEQ_1:1;
then i in Seg (len (x1 + x2)) by A1, Th2;
then i in dom (x1 + x2) by FINSEQ_1:def 3;
hence (x1 + x2) . i = (x1 /. i) + (x2 /. i) by A3, FVSUM_1:17; :: thesis: (x1 - x2) . i = (x1 /. i) - (x2 /. i)
i in Seg (len x1) by A2, FINSEQ_1:1;
then i in Seg (len (x1 - x2)) by A1, Th3;
then i in dom (x1 - x2) by FINSEQ_1:def 3;
hence (x1 - x2) . i = (x1 /. i) - (x2 /. i) by A3, FVSUM_1:32; :: thesis: verum