set F = SeqField f;

A: now :: thesis: for x, y being Element of (SeqField f) holds x * y = y * x

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 & (multseq f) . (b,a) = yi * xi ) by defmult;
thus x * y = xi * yi by A, lem4
.= yi * xi by GROUP_1:def 12
.= y * x by A, lem4 ; :: thesis: verum

end;

hence SeqField f is commutative ; :: thesis: ( SeqField f is associative & SeqField f is well-unital & SeqField f is distributive & SeqField f is almost_left_invertible )

hereby :: according to GROUP_1:def 3 :: thesis: ( SeqField f is well-unital & SeqField f is distributive & SeqField f is almost_left_invertible )

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 & (multseq f) . (a,b) = xi * yi ) by defmult;
consider j being Element of NAT , xj, zj being Element of (f . j) such that
B: ( xj = ab & zj = c & (multseq f) . (ab,c) = xj * zj ) by defmult;

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 GROUP_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 GROUP_1:def 3
.= x * (y * z) by A, C, lem4 ;
:: thesis: verum

end;

end;

end;

hereby :: according to VECTSP_1:def 6 :: thesis: ( SeqField f is distributive & SeqField f is almost_left_invertible )

let x be Element of (SeqField f); :: thesis: ( x * (1. (SeqField f)) = x & (1. (SeqField f)) * x = 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;
C: 1. (SeqField f) = 1. (f . i) by lem5;
thus x * (1. (SeqField f)) = a * (1. (f . i)) by C, lem4
.= x ; :: thesis: (1. (SeqField f)) * x = x
thus (1. (SeqField f)) * x = (1. (f . i)) * a by C, lem4
.= x ; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 7 :: thesis: SeqField f is almost_left_invertible

let x, y, z be Element of (SeqField f); :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider a = x, b = y, c = z, bc = y + z as Element of Carrier f by dsf;
consider i being Element of NAT , yi, zi being Element of (f . i) such that
B: ( yi = b & zi = c & (addseq f) . (b,c) = yi + zi ) by defadd;
consider j being Element of NAT , xj, pj being Element of (f . j) such that
C: ( xj = a & pj = bc & (multseq f) . (a,bc) = xj * pj ) by defmult;
thus Z: x * (y + z) = (x * y) + (x * z) :: thesis: (y + z) * x = (y * x) + (z * x)

proof

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

suppose j <= i ; :: thesis: x * (y + z) = (x * y) + (x * z)

then reconsider xi = xj as Element of (f . i) by lem1;
D: ( x * y = xi * yi & x * z = xi * zi ) by B, C, lem4;
y + z = yi + zi by B, lem4;
hence x * (y + z) = xi * (yi + zi) by C, lem4
.= (xi * yi) + (xi * zi) by VECTSP_1:def 2
.= (x * y) + (x * z) by D, lem4 ;
:: thesis: verum

end;

suppose i <= j ; :: thesis: x * (y + z) = (x * y) + (x * z)

then reconsider yj = yi, zj = zi as Element of (f . j) by lem1;
D: ( x * y = xj * yj & x * z = xj * zj ) by B, C, lem4;
y + z = yj + zj by B, lem4;
hence x * (y + z) = xj * (yj + zj) by C, lem4
.= (xj * yj) + (xj * zj) by VECTSP_1:def 2
.= (x * y) + (x * z) by D, lem4 ;
:: thesis: verum

end;

end;

end;

thus (y + z) * x = (x * y) + (x * z) by A, Z
.= (x * y) + (z * x) by A
.= (y * x) + (z * x) by A ; :: thesis: verum

end;

let x be Element of (SeqField f); :: according to VECTSP_1:def 9 :: thesis: ( x = 0. (SeqField f) or ex b₁ being Element of the carrier of (SeqField f) st b₁ * x = 1. (SeqField f) )
assume H: x <> 0. (SeqField f) ; :: thesis: ex b₁ being Element of the carrier of (SeqField f) st b₁ * x = 1. (SeqField f)
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;
C: a <> 0. (f . i) by H, lem5;
take y ; :: thesis: y * x = 1. (SeqField f)
thus y * x = (a ") * a by lem4
.= 1. (f . i) by C, VECTSP_1:def 10
.= 1. (SeqField f) by lem5 ; :: thesis: verum