let i, j be Element of 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:65;
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 set ; :: 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 set 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 set ; :: 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:56
.= <*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:56
.= <*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:66; :: thesis: verum

end;

dom <*r,s*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
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:18; :: thesis: verum

end;

let c be set ; :: 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 set 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:66;
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:66;
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 set st k in dom g holds
g . k = <*a,b*> . k

proof

let k be set ; :: 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:61; :: thesis: verum

end;

dom <*a,b*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then c = |[a,b]| by A11, A12, A18, FUNCT_1:9, FUNCT_4:65;
hence c in cell G,i,j by A3, A17, A15; :: thesis: verum