let x, y, z, a, b be Element of {0,1,2}; :: thesis: ( a = 0 & b = 1 implies ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) ) )

assume that

A1: a = 0 and

A2: b = 1 ; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x + y = y + x :: thesis: ( (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x + a = x by A1, Def13; :: thesis: ( x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x + (- x) = a by A1, Lm7; :: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x * y = y * x :: thesis: ( (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) :: thesis: ( a <> b & x * (y + z) = (x * y) + (x * z) )

thus x * (y + z) = (x * y) + (x * z) :: thesis: verum

assume that

A1: a = 0 and

A2: b = 1 ; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x + y = y + x :: thesis: ( (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof

end;

thus
(x + y) + z = x + (y + z)
by A1, Lm7; :: thesis: ( x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )now :: thesis: x + y = y + xend;

hence
x + y = y + x
; :: thesis: verumper cases
( x = 0 or y = 0 or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) )
by ENUMSET1:def 1;

end;

thus x + a = x by A1, Def13; :: thesis: ( x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x + (- x) = a by A1, Lm7; :: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

thus x * y = y * x :: thesis: ( (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof

end;

thus
(x * y) * z = x * (y * z)
:: thesis: ( b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )now :: thesis: x * y = y * x

hence
x * y = y * x
; :: thesis: verumend;

proof

end;

thus
b * x = x
by A2, Def14; :: thesis: ( ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )now :: thesis: (x * y) * z = x * (y * z)end;

hence
(x * y) * z = x * (y * z)
; :: thesis: verumper cases
( z = 0 or y = 0 or x = 0 or z = 1 or y = 1 or x = 1 or ( x = 2 & y = 2 & z = 2 ) )
by ENUMSET1:def 1;

end;

suppose A11:
z = 0
; :: thesis: (x * y) * z = x * (y * z)

then A12:
y * z = 0
by Def14;

thus (x * y) * z = 0 by A11, Def14

.= x * (y * z) by A12, Def14 ; :: thesis: verum

end;thus (x * y) * z = 0 by A11, Def14

.= x * (y * z) by A12, Def14 ; :: thesis: verum

suppose A13:
y = 0
; :: thesis: (x * y) * z = x * (y * z)

then A14:
y * z = 0
by Def14;

x * y = 0 by A13, Def14;

hence (x * y) * z = 0 by Def14

.= x * (y * z) by A14, Def14 ;

:: thesis: verum

end;x * y = 0 by A13, Def14;

hence (x * y) * z = 0 by Def14

.= x * (y * z) by A14, Def14 ;

:: thesis: verum

suppose A15:
x = 0
; :: thesis: (x * y) * z = x * (y * z)

then
x * y = 0
by Def14;

hence (x * y) * z = 0 by Def14

.= x * (y * z) by A15, Def14 ;

:: thesis: verum

end;hence (x * y) * z = 0 by Def14

.= x * (y * z) by A15, Def14 ;

:: thesis: verum

thus ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) :: thesis: ( a <> b & x * (y + z) = (x * y) + (x * z) )

proof

end;

thus
a <> b
by A1, A2; :: thesis: x * (y + z) = (x * y) + (x * z)now :: thesis: ( ( x = 0 & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) or ( x = 1 & ex y being Element of {0,1,2} st

( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) or ( x = 2 & ex y being Element of {0,1,2} st

( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) )end;

hence
( x <> a implies ex y being Element of {0,1,2} st x * y = b )
; :: thesis: verum( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) or ( x = 2 & ex y being Element of {0,1,2} st

( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) )

per cases
( x = 0 or x = 1 or x = 2 )
by ENUMSET1:def 1;

end;

case A21:
x = 1
; :: thesis: ex y being Element of {0,1,2} st

( x <> a implies ex y being Element of {0,1,2} st x * y = b )

( x <> a implies ex y being Element of {0,1,2} st x * y = b )

reconsider y = 1 as Element of {0,1,2} by ENUMSET1:def 1;

take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )

x * y = 1 by A21, Def14;

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

end;take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )

x * y = 1 by A21, Def14;

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

case A22:
x = 2
; :: thesis: ex y being Element of {0,1,2} st

( x <> a implies ex y being Element of {0,1,2} st x * y = b )

( x <> a implies ex y being Element of {0,1,2} st x * y = b )

reconsider y = 2 as Element of {0,1,2} by ENUMSET1:def 1;

take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )

x * y = 1 by A22, Def14;

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

end;take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )

x * y = 1 by A22, Def14;

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

thus x * (y + z) = (x * y) + (x * z) :: thesis: verum

proof

end;

now :: thesis: x * (y + z) = (x * y) + (x * z)end;

hence
x * (y + z) = (x * y) + (x * z)
; :: thesis: verumper cases
( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) )
by ENUMSET1:def 1;

end;

suppose A23:
x = 0
; :: thesis: x * (y + z) = (x * y) + (x * z)

then A24:
( x * y = 0 & x * z = 0 )
by Def14;

thus x * (y + z) = 0 by A23, Def14

.= (x * y) + (x * z) by A24, Def13 ; :: thesis: verum

end;thus x * (y + z) = 0 by A23, Def14

.= (x * y) + (x * z) by A24, Def13 ; :: thesis: verum

suppose
y = 0
; :: thesis: x * (y + z) = (x * y) + (x * z)

then
( y + z = z & x * y = 0 )
by Def13, Def14;

hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

end;hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

suppose
z = 0
; :: thesis: x * (y + z) = (x * y) + (x * z)

then
( y + z = y & x * z = 0 )
by Def13, Def14;

hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

end;hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

suppose A26:
( x = 1 & y = 1 & z = 2 )
; :: thesis: x * (y + z) = (x * y) + (x * z)

then A27:
( x * y = 1 & x * z = 2 )
by Def14;

y + z = 0 by A26, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A27, Def13 ;

:: thesis: verum

end;y + z = 0 by A26, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A27, Def13 ;

:: thesis: verum

suppose A28:
( x = 1 & y = 2 & z = 1 )
; :: thesis: x * (y + z) = (x * y) + (x * z)

then A29:
( x * y = 2 & x * z = 1 )
by Def14;

y + z = 0 by A28, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A29, Def13 ;

:: thesis: verum

end;y + z = 0 by A28, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A29, Def13 ;

:: thesis: verum

suppose A31:
( x = 2 & y = 1 & z = 1 )
; :: thesis: x * (y + z) = (x * y) + (x * z)

then A32:
x * y = 2
by Def14;

y + z = 2 by A31, Def13;

hence x * (y + z) = 1 by A31, Def14

.= (x * y) + (x * z) by A31, A32, Def13 ;

:: thesis: verum

end;y + z = 2 by A31, Def13;

hence x * (y + z) = 1 by A31, Def14

.= (x * y) + (x * z) by A31, A32, Def13 ;

:: thesis: verum

suppose A33:
( x = 2 & y = 1 & z = 2 )
; :: thesis: x * (y + z) = (x * y) + (x * z)

then A34:
( x * y = 2 & x * z = 1 )
by Def14;

y + z = 0 by A33, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A34, Def13 ;

:: thesis: verum

end;y + z = 0 by A33, Def13;

hence x * (y + z) = 0 by Def14

.= (x * y) + (x * z) by A34, Def13 ;

:: thesis: verum