let i be Element of NAT ; :: thesis: for G being Go-board st 1 <= i & i <= len G holds
(SgmX RealOrd ,(proj1 .: (Values G))) . i = (G * i,1) `1
let G be Go-board; :: thesis: ( 1 <= i & i <= len G implies (SgmX RealOrd ,(proj1 .: (Values G))) . i = (G * i,1) `1 )
assume A1:
( 1 <= i & i <= len G )
; :: thesis: (SgmX RealOrd ,(proj1 .: (Values G))) . i = (G * i,1) `1
deffunc H1( Nat) -> Element of REAL = (G * $1,1) `1 ;
consider f being FinSequence of REAL such that
A2:
len f = len G
and
A3:
for i being Nat st i in dom f holds
f . i = H1(i)
from FINSEQ_2:sch 1();
A4:
dom f = Seg (len G)
by A2, FINSEQ_1:def 3;
0 <> width G
by GOBOARD1:def 5;
then A5:
1 <= width G
by NAT_1:14;
reconsider A = proj1 .: (Values G) as finite Subset of REAL ;
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
:: according to XBOOLE_0:def 10 :: thesis: A c= rng fproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in A )
assume A8:
x in rng f
;
:: thesis: 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 <= len G )
by A2, A9, FINSEQ_3:27;
then
[y,1] in Indices G
by A5, MATRIX_1:37;
then A11:
G * y,1
in Values G
by A7;
y in Seg (len G)
by A2, A9, FINSEQ_1:def 3;
then x =
(G * y,1) `1
by A3, A10, A4
.=
proj1 . (G * y,1)
by PSCOMP_1:def 28
;
hence
x in A
by A11, FUNCT_2:43;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng f )
assume A12:
x in A
;
:: thesis: 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 = proj1 . 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
<= n &
n <= width G )
by A16, MATRIX_1:39;
A18:
( 1
<= m &
m <= len G )
by A16, MATRIX_1:39;
then A19:
m in Seg (len G)
by FINSEQ_1:3;
A20:
m in dom f
by A2, A18, FINSEQ_3:27;
x =
p `1
by A14, PSCOMP_1:def 28
.=
(G * m,1) `1
by A15, A17, A18, GOBOARD5:3
.=
f . m
by A3, A19, A4
;
hence
x in rng f
by A20, FUNCT_1:def 5;
:: thesis: 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 ;
:: thesis: ( 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
and A22:
m in dom f
and A23:
n < m
;
:: thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
reconsider n' =
n,
m' =
m as
Element of
NAT by ORDINAL1:def 13;
A24:
(
f . n = (G * n',1) `1 &
f . m = (G * m',1) `1 )
by A3, A21, A22;
A25:
( 1
<= n &
m <= len G )
by A2, A21, A22, FINSEQ_3:27;
then A26:
f . n' < f . m'
by A5, A23, A24, GOBOARD5:4;
A27:
(
f /. n = f . n &
f /. m = f . m )
by A21, A22, PARTFUN1:def 8;
hence
f /. n <> f /. m
by A5, A23, A24, A25, GOBOARD5:4;
:: thesis: [(f /. n),(f /. m)] in RealOrd
thus
[(f /. n),(f /. m)] in RealOrd
by A26, A27;
:: thesis: verum
end;
then A28:
f = SgmX RealOrd ,(proj1 .: (Values G))
by A6, TRIANG_1:4;
i in dom G
by A1, FINSEQ_3:27;
then
i in Seg (len G)
by FINSEQ_1:def 3;
hence
(SgmX RealOrd ,(proj1 .: (Values G))) . i = (G * i,1) `1
by A3, A28, A4; :: thesis: verum