let i, j be Nat; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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).])) :: according to XBOOLE_0:def 10 :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: ( 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).])) ; :: thesis: <*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; :: thesis: 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; :: thesis: verum
end;
let c be object ; :: according to TARSKI:def 3 :: thesis: ( 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).])) ; :: thesis: 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
proof
let k be object ; :: thesis: ( k in dom g implies g . k = <*a,b*> . k )
assume k in dom g ; :: thesis: g . k = <*a,b*> . k
then ( k = 1 or k = 2 ) by A12, TARSKI:def 2;
hence g . k = <*a,b*> . k by A16, A14, FINSEQ_1:44; :: thesis: verum
end;
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; :: thesis: verum