let j be Element of NAT ; for G being Go-board st 1 <= j & j <= width G holds
(SgmX RealOrd ,(proj2 .: (Values G))) . j = (G * 1,j) `2
let G be Go-board; ( 1 <= j & j <= width G implies (SgmX RealOrd ,(proj2 .: (Values G))) . j = (G * 1,j) `2 )
assume
( 1 <= j & j <= width G )
; (SgmX RealOrd ,(proj2 .: (Values G))) . j = (G * 1,j) `2
then A1:
j in Seg (width G)
by FINSEQ_1:3;
0 <> len G
by GOBOARD1:def 5;
then A2:
1 <= len G
by NAT_1:14;
reconsider A = proj2 .: (Values G) as finite Subset of REAL ;
deffunc H1( Nat) -> Element of REAL = (G * 1,$1) `2 ;
consider f being FinSequence of REAL such that
A3:
len f = width G
and
A4:
for i being Nat st i in dom f holds
f . i = H1(i)
from FINSEQ_2:sch 1();
A5:
dom f = Seg (width G)
by A3, FINSEQ_1:def 3;
A6:
rng f = A
proof
A7:
Values G = { (G * m,n) where m, n is Element of NAT : [m,n] in Indices G }
by GOBRD13:7;
thus
rng f c= A
XBOOLE_0:def 10 A c= rng fproof
let x be
set ;
TARSKI:def 3 ( not x in rng f or x in A )
assume A8:
x in rng f
;
x in A
then reconsider x =
x as
Element of
REAL ;
consider y being
set such that A9:
y in dom f
and A10:
x = f . y
by A8, FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A9;
( 1
<= y &
y <= width G )
by A3, A9, FINSEQ_3:27;
then
[1,y] in Indices G
by A2, MATRIX_1:37;
then A11:
G * 1,
y in Values G
by A7;
x =
(G * 1,y) `2
by A4, A9, A10
.=
proj2 . (G * 1,y)
by PSCOMP_1:def 29
;
hence
x in A
by A11, FUNCT_2:43;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in A or x in rng f )
assume A12:
x in A
;
x in rng f
then reconsider x =
x as
Element of
REAL ;
consider p being
Element of
(TOP-REAL 2) such that A13:
p in Values G
and A14:
x = proj2 . p
by A12, FUNCT_2:116;
consider m,
n being
Element of
NAT such that A15:
p = G * m,
n
and A16:
[m,n] in Indices G
by A7, A13;
A17:
( 1
<= m &
m <= len G )
by A16, MATRIX_1:39;
A18:
( 1
<= n &
n <= width G )
by A16, MATRIX_1:39;
then A19:
n in Seg (width G)
by FINSEQ_1:3;
A20:
n in dom f
by A3, A18, FINSEQ_3:27;
x =
p `2
by A14, PSCOMP_1:def 29
.=
(G * 1,n) `2
by A15, A17, A18, GOBOARD5:2
.=
f . n
by A4, A5, A19
;
hence
x in rng f
by A20, FUNCT_1:def 5;
verum
end;
for n, m being natural number st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
proof
let n,
m be
natural number ;
( n in dom f & m in dom f & n < m implies ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) )
assume that A21:
(
n in dom f &
m in dom f )
and A22:
n < m
;
( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
A23:
( 1
<= n &
m <= width G )
by A3, A21, FINSEQ_3:27;
reconsider n9 =
n,
m9 =
m as
Element of
NAT by ORDINAL1:def 13;
A24:
(
f /. n = f . n &
f /. m = f . m )
by A21, PARTFUN1:def 8;
A25:
(
f . n = (G * 1,n9) `2 &
f . m = (G * 1,m9) `2 )
by A4, A21;
hence
f /. n <> f /. m
by A2, A22, A23, A24, GOBOARD5:5;
[(f /. n),(f /. m)] in RealOrd
f . n9 < f . m9
by A2, A22, A25, A23, GOBOARD5:5;
hence
[(f /. n),(f /. m)] in RealOrd
by A24;
verum
end;
then
f = SgmX RealOrd ,(proj2 .: (Values G))
by A6, PRE_POLY:9;
hence
(SgmX RealOrd ,(proj2 .: (Values G))) . j = (G * 1,j) `2
by A4, A5, A1; verum