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 A1: ( len x1 = len x2 & 1 <= i & i <= len x1 ) ; :: thesis: ( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )
then reconsider x10 = x1, x20 = x2 as Element of (len x1) -tuples_on the carrier of L by BB100;
i in Seg (len x1) by A1, FINSEQ_1:3;
then A3: i in Seg (len (x1 + x2)) by A1, Th6;
A4: x10 /. i = x10 . i by A1, FINSEQ_4:24;
A5: x20 /. i = x20 . i by A1, FINSEQ_4:24;
i in dom (x1 + x2) by A3, FINSEQ_1:def 3;
hence (x1 + x2) . i = (x1 /. i) + (x2 /. i) by A4, A5, FVSUM_1:21; :: thesis: (x1 - x2) . i = (x1 /. i) - (x2 /. i)
i in Seg (len x1) by A1, FINSEQ_1:3;
then i in Seg (len (x1 - x2)) by A1, Th7;
then i in dom (x1 - x2) by FINSEQ_1:def 3;
hence (x1 - x2) . i = (x1 /. i) - (x2 /. i) by A4, A5, FVSUM_1:42; :: thesis: verum