set F = Z_3 ;

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

(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

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) )

then reconsider F = Z_3 as Field by Th26;( 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

end;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) )

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;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

thus
0. Z_3 <> 1. Z_3
; :: thesis: x * (y + z) = (x * y) + (x * z)
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;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

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

(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