set F = SeqField f;

hereby :: according to RLVECT_1:def 2 :: thesis: ( SeqField f is add-associative & SeqField f is right_zeroed & SeqField f is right_complementable )

let x, y be Element of (SeqField f); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of Carrier f by dsf;
consider i being Element of NAT , yi, xi being Element of (f . i) such that
A: ( yi = b & xi = a & (addseq f) . (b,a) = yi + xi ) by defadd;
thus x + y = xi + yi by A, lem4
.= y + x by A, lem4 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( SeqField f is right_zeroed & SeqField f is right_complementable )

let x, y, z be Element of (SeqField f); :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)
reconsider a = x, b = y, c = z, ab = x + y as Element of Carrier f by dsf;
consider i being Element of NAT , xi, yi being Element of (f . i) such that
A: ( xi = a & yi = b & (addseq f) . (a,b) = xi + yi ) by defadd;
consider j being Element of NAT , xj, zj being Element of (f . j) such that
B: ( xj = ab & zj = c & (addseq f) . (ab,c) = xj + zj ) by defadd;

per cases ( j <= i or i <= j ) ;

suppose j <= i ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then reconsider zi = zj as Element of (f . i) by lem1;
C: yi + zi = y + z by A, B, lem4;
x + y = xi + yi by A, lem4;
hence (x + y) + z = (xi + yi) + zi by B, lem4
.= xi + (yi + zi) by RLVECT_1:def 3
.= x + (y + z) by A, C, lem4 ;
:: thesis: verum

end;

suppose i <= j ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then reconsider xj = xi, yj = yi as Element of (f . j) by lem1;
C: yj + zj = y + z by A, B, lem4;
x + y = xj + yj by A, lem4;
hence (x + y) + z = (xj + yj) + zj by B, lem4
.= xj + (yj + zj) by RLVECT_1:def 3
.= x + (y + z) by A, C, lem4 ;
:: thesis: verum

end;

end;

end;

hereby :: according to RLVECT_1:def 4 :: thesis: SeqField f is right_complementable

let x be Element of (SeqField f); :: thesis: x + (0. (SeqField f)) = x
x is Element of Carrier f by dsf;
then consider Y being set such that
A: ( x in Y & Y in { the carrier of (f . i) where i is Element of NAT : verum } ) by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of (f . i) by A;
reconsider a = x as Element of (f . i) by A, B;
0. (SeqField f) = 0. (f . i) by lem5;
hence x + (0. (SeqField f)) = a + (0. (f . i)) by lem4
.= x ;
:: thesis: verum

end;

let x be Element of (SeqField f); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
x is Element of Carrier f by dsf;
then consider Y being set such that
A: ( x in Y & Y in { the carrier of (f . i) where i is Element of NAT : verum } ) by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of (f . i) by A;
reconsider a = x as Element of (f . i) by A, B;
the carrier of (f . i) in { the carrier of (f . i) where i is Element of NAT : verum } ;
then - a in Carrier f by TARSKI:def 4;
then reconsider y = - a as Element of (SeqField f) by dsf;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (SeqField f)
thus x + y = a + (- a) by lem4
.= 0. (f . i) by RLVECT_1:5
.= 0. (SeqField f) by lem5 ; :: thesis: verum