let i, j be Nat; for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell (G,i,j) = product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
let G be Go-board; ( 1 <= i & i < len G & 1 <= j & j < width G implies cell (G,i,j) = product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) )
A1:
[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).] = { b where b is Real : ( (G * (1,j)) `2 <= b & b <= (G * (1,(j + 1))) `2 ) }
by RCOMP_1:def 1;
set f = (1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]);
A2:
dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) = {1,2}
by FUNCT_4:62;
assume
( 1 <= i & i < len G & 1 <= j & j < width G )
; cell (G,i,j) = product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
then A3:
cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) }
by GOBRD11:32;
A4:
[.((G * (i,1)) `1),((G * ((i + 1),1)) `1).] = { a where a is Real : ( (G * (i,1)) `1 <= a & a <= (G * ((i + 1),1)) `1 ) }
by RCOMP_1:def 1;
thus
cell (G,i,j) c= product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
XBOOLE_0:def 10 product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) c= cell (G,i,j)proof
let c be
object ;
TARSKI:def 3 ( not c in cell (G,i,j) or c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) )
assume
c in cell (
G,
i,
j)
;
c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
then consider r,
s being
Real such that A5:
c = |[r,s]|
and A6:
(
(G * (i,1)) `1 <= r &
r <= (G * ((i + 1),1)) `1 &
(G * (1,j)) `2 <= s &
s <= (G * (1,(j + 1))) `2 )
by A3;
A7:
(
r in [.((G * (i,1)) `1),((G * ((i + 1),1)) `1).] &
s in [.((G * (1,j)) `2),((G * (1,(j + 1))) `2).] )
by A4, A1, A6;
A8:
for
x being
object st
x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds
<*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
proof
let x be
object ;
( x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) implies <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x )
A9:
s =
|[r,s]| `2
by EUCLID:52
.=
<*r,s*> . 2
;
assume
x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
;
<*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
then A10:
(
x = 1 or
x = 2 )
by TARSKI:def 2;
r =
|[r,s]| `1
by EUCLID:52
.=
<*r,s*> . 1
;
hence
<*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
by A7, A10, A9, FUNCT_4:63;
verum
end;
dom <*r,s*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
hence
c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
by A2, A5, A8, CARD_3:9;
verum
end;
let c be object ; TARSKI:def 3 ( not c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) or c in cell (G,i,j) )
assume
c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
; c in cell (G,i,j)
then consider g being Function such that
A11:
c = g
and
A12:
dom g = dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
and
A13:
for x being object st x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds
g . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
by CARD_3:def 5;
2 in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
by A2, TARSKI:def 2;
then
g . 2 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 2
by A13;
then
g . 2 in [.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]
by FUNCT_4:63;
then consider b being Real such that
A14:
g . 2 = b
and
A15:
( (G * (1,j)) `2 <= b & b <= (G * (1,(j + 1))) `2 )
by A1;
1 in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
by A2, TARSKI:def 2;
then
g . 1 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 1
by A13;
then
g . 1 in [.((G * (i,1)) `1),((G * ((i + 1),1)) `1).]
by FUNCT_4:63;
then consider a being Real such that
A16:
g . 1 = a
and
A17:
( (G * (i,1)) `1 <= a & a <= (G * ((i + 1),1)) `1 )
by A4;
A18:
for k being object st k in dom g holds
g . k = <*a,b*> . k
dom <*a,b*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then
c = |[a,b]|
by A11, A12, A18, FUNCT_1:2, FUNCT_4:62;
hence
c in cell (G,i,j)
by A3, A17, A15; verum