let j be 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:1;
A2:
1 <= len G
by NAT_1:14;
reconsider A = proj2 .: (Values G) as finite Subset of REAL ;
deffunc H1( Nat) -> Element of REAL = In (((G * (1,$1)) `2),REAL);
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 Nat : [m,n] in Indices G }
by MATRIX_0:39;
thus
rng f c= A
XBOOLE_0:def 10 A c= rng fproof
let x be
object ;
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
object such that A9:
y in dom f
and A10:
x = f . y
by A8, FUNCT_1:def 3;
reconsider y =
y as
Nat by A9;
( 1
<= y &
y <= width G )
by A3, A9, FINSEQ_3:25;
then
[1,y] in Indices G
by A2, MATRIX_0:30;
then A11:
G * (1,
y)
in Values G
by A7;
x =
H1(
y)
by A4, A9, A10
.=
proj2 . (G * (1,y))
by PSCOMP_1:def 6
;
hence
x in A
by A11, FUNCT_2:35;
verum
end;
let x be
object ;
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:65;
consider m,
n being
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_0:32;
A18:
( 1
<= n &
n <= width G )
by A16, MATRIX_0:32;
then A19:
n in Seg (width G)
by FINSEQ_1:1;
A20:
n in dom f
by A3, A18, FINSEQ_3:25;
x =
p `2
by A14, PSCOMP_1:def 6
.=
H1(
n)
by A15, A17, A18, GOBOARD5:1
.=
f . n
by A4, A5, A19
;
hence
x in rng f
by A20, FUNCT_1:def 3;
verum
end;
for n, m being Nat 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
Nat;
( 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:25;
reconsider n9 =
n,
m9 =
m as
Nat ;
A24:
(
f /. n = f . n &
f /. m = f . m )
by A21, PARTFUN1:def 6;
A25:
(
f . n = H1(
n9) &
f . m = H1(
m9) )
by A4, A21;
hence
f /. n <> f /. m
by A2, A22, A23, A24, GOBOARD5:4;
[(f /. n),(f /. m)] in RealOrd
f . n9 < f . m9
by A2, A22, A25, A23, GOBOARD5:4;
hence
[(f /. n),(f /. m)] in RealOrd
by A24;
verum
end;
then
f = SgmX (RealOrd,(proj2 .: (Values G)))
by A6, PRE_POLY:9;
then
(SgmX (RealOrd,(proj2 .: (Values G)))) . j = H1(j)
by A4, A5, A1;
hence
(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2
; verum