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

now

let x, y, z be Scalar of Z3 ; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z3 ) = x & x + (- x) = 0. Z3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z3 ) = x & x + (- x) = 0. Z3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & 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 Th33;
thus x + y = X + Y by Th33
.= Y + X by Th35
.= y + x by Th33 ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. Z3 ) = x & x + (- x) = 0. Z3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus (x + y) + z = (X + Y) + Z by Th34
.= X + (Y + Z) by Th35
.= x + (y + z) by Th34 ; :: thesis: ( x + (0. Z3 ) = x & x + (- x) = 0. Z3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus x + (0. Z3 ) = X + a by Th33
.= x by Th35 ; :: thesis: ( x + (- x) = 0. Z3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
- x = - X by Th33;
hence x + (- x) = X + (- X) by Th33
.= 0. Z3 by Th35 ;
:: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus x * y = X * Y by Th33
.= Y * X by Th35
.= y * x by Th33 ; :: thesis: ( (x * y) * z = x * (y * z) & (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus (x * y) * z = (X * Y) * Z by Th34
.= X * (Y * Z) by Th35
.= x * (y * z) by Th34 ; :: thesis: ( (1. Z3 ) * x = x & x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus (1. Z3 ) * x = b * X by Th33
.= x by Th35 ; :: thesis: ( x * (1. Z3 ) = x & ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus x * (1. Z3 ) = X * b by Th33
.= b * X by Th35
.= x by Th35 ; :: thesis: ( ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) & 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )
thus ( x <> 0. Z3 implies ex y being Scalar of Z3 st x * y = 1. Z3 ) :: thesis: ( 0. Z3 <> 1. Z3 & x * (y + z) = (x * y) + (x * z) )

proof

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

end;

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

end;

end;

then reconsider F = Z3 as Field by Th36;
(1. F) + (1. F) = b + b by Def18
.= 2 by Def16 ;
hence Z3 is Fanoian Field by Th32, VECTSP_1:def 29; :: thesis: verum