let i be 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 ( 1 <= i & i <= len G ) ; :: thesis: (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1
then i in dom G by FINSEQ_3:25;
then A1: i in Seg (len G) by FINSEQ_1:def 3;
0 <> width G by MATRIX_0:def 10;
then A2: 1 <= width G by NAT_1:14;
reconsider A = proj1 .: (Values G) as finite Subset of REAL ;
deffunc H<sub>1</sub>( Nat) -> Element of REAL = In (((G * ($1,1)) `1),REAL);
consider f being FinSequence of REAL such that
A3: len f = len G and
A4: for i being Nat st i in dom f holds
f . i = H₁(i) from FINSEQ_2:sch 1();
A5: dom f = Seg (len 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 :: according to XBOOLE_0:def 10 :: thesis: A c= rng f

proof

let x be object ; :: 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 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 <= len G ) by A3, A9, FINSEQ_3:25;
then [y,1] in Indices G by A2, MATRIX_0:30;
then A11: G * (y,1) in Values G by A7;
x = H₁(y) by A4, A9, A10
.= proj1 . (G * (y,1)) by PSCOMP_1:def 5 ;
hence x in A by A11, FUNCT_2:35; :: thesis: verum

end;

let x be object ; :: 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: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 <= n & n <= width G ) by A16, MATRIX_0:32;
A18: ( 1 <= m & m <= len G ) by A16, MATRIX_0:32;
then A19: m in Seg (len G) by FINSEQ_1:1;
A20: m in dom f by A3, A18, FINSEQ_3:25;
x = p `1 by A14, PSCOMP_1:def 5
.= H₁(m) by A15, A17, A18, GOBOARD5:2
.= f . m by A4, A5, A19 ;
hence x in rng f by A20, FUNCT_1:def 3; :: thesis: 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; :: 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 & m in dom f ) and
A22: n < m ; :: thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
A23: ( 1 <= n & m <= len 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 = H₁(n9) & f . m = H₁(m9) ) by A4, A21;
hence f /. n <> f /. m by A2, A22, A23, A24, GOBOARD5:3; :: thesis: [(f /. n),(f /. m)] in RealOrd
f . n9 < f . m9 by A2, A22, A25, A23, GOBOARD5:3;
hence [(f /. n),(f /. m)] in RealOrd by A24; :: thesis: verum

end;

then f = SgmX (RealOrd,(proj1 .: (Values G))) by A6, PRE_POLY:9;
then (SgmX (RealOrd,(proj1 .: (Values G)))) . i = H₁(i) by A4, A5, A1;
hence (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 ; :: thesis: verum