set F = Z_3 ;
reconsider a = 0. Z_3, b = 1. Z_3 as Element of {0,1,2} ;

now :: thesis: for x, y, z being Scalar of Z_3 holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )

let x, y, z be Scalar of Z_3; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) ) :: thesis: verum

proof

reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;
A1: ( x * y = X * Y & x * z = X * Z ) by Th23;
thus x + y = X + Y by Th23
.= Y + X by Th25
.= y + x by Th23 ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x + y) + z = (X + Y) + Z by Th24
.= X + (Y + Z) by Th25
.= x + (y + z) by Th24 ; :: thesis: ( x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x + (0. Z_3) = X + a by Th23
.= x by Th25 ; :: thesis: ( x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
- x = - X by Th23;
hence x + (- x) = X + (- X) by Th23
.= 0. Z_3 by Th25 ;
:: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * y = X * Y by Th23
.= Y * X by Th25
.= y * x by Th23 ; :: thesis: ( (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x * y) * z = (X * Y) * Z by Th24
.= X * (Y * Z) by Th25
.= x * (y * z) by Th24 ; :: thesis: ( (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (1. Z_3) * x = b * X by Th23
.= x by Th25 ; :: thesis: ( x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * (1. Z_3) = X * b by Th23
.= b * X by Th25
.= x by Th25 ; :: thesis: ( ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) :: thesis: ( 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )

proof

assume x <> 0. Z_3 ; :: thesis: ex y being Scalar of Z_3 st x * y = 1. Z_3
then consider Y being Element of {0,1,2} such that
A2: X * Y = b by Th25;
reconsider y = Y as Scalar of Z_3 ;
take y ; :: thesis: x * y = 1. Z_3
thus x * y = 1. Z_3 by A2, Th23; :: thesis: verum

end;

thus 0. Z_3 <> 1. Z_3 ; :: thesis: x * (y + z) = (x * y) + (x * z)
y + z = Y + Z by Th23;
hence x * (y + z) = X * (Y + Z) by Th23
.= (X * Y) + (X * Z) by Th25
.= (x * y) + (x * z) by A1, Th23 ;
:: thesis: verum

end;

end;

then reconsider F = Z_3 as Field by Th26;
(1. F) + (1. F) = b + b by Def15
.= 2 by Def13 ;
hence Z_3 is Fanoian Field by Th22, VECTSP_1:def 19; :: thesis: verum