let f be non empty FinSequence of (TOP-REAL 2); for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
set x = X_axis f;
set y = Y_axis f;
let n be Nat; ( n in dom f implies ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) )
assume A1:
n in dom f
; ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
A2:
rng (Incr (Y_axis f)) = rng (Y_axis f)
by SEQ_4:def 21;
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3:
dom f = Seg (len f)
by FINSEQ_1:def 3;
( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f )
by FINSEQ_1:def 3, GOBOARD1:def 2;
then
( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) )
by A1, A3, FUNCT_1:def 3, GOBOARD1:def 2;
then consider j being Nat such that
A4:
j in dom (Incr (Y_axis f))
and
A5:
(Incr (Y_axis f)) . j = p `2
by A2, FINSEQ_2:10;
A6:
rng (Incr (X_axis f)) = rng (X_axis f)
by SEQ_4:def 21;
( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f )
by FINSEQ_1:def 3, GOBOARD1:def 1;
then
( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) )
by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;
then consider i being Nat such that
A7:
i in dom (Incr (X_axis f))
and
A8:
(Incr (X_axis f)) . i = p `1
by A6, FINSEQ_2:10;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) )
by Th13, SEQ_4:def 21;
then A9:
Seg (width (GoB f)) = dom (Incr (Y_axis f))
by FINSEQ_1:def 3;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 12;
take
i
; ex j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
take
j
; ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) )
by Th13, SEQ_4:def 21;
then
( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (GoB f) = dom (Incr (X_axis f)) )
by FINSEQ_3:29, MATRIX_0:def 4;
hence
[i,j] in Indices (GoB f)
by A7, A4, A9, ZFMISC_1:87; f /. n = (GoB f) * (i,j)
then
(GoB f) * (i,j) = |[(p `1),(p `2)]|
by A8, A5, Def1;
hence
f /. n = (GoB f) * (i,j)
by EUCLID:53; verum