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) )
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:
GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f)))
by GOBOARD2:def 2;
set x = (f /. n) `1 ;
set y = (f /. n) `2 ;
A3:
n in dom (X_axis f)
by A1, Lm1;
then
(X_axis f) . n = (f /. n) `1
by GOBOARD1:def 1;
then
(f /. n) `1 in rng (X_axis f)
by A3, FUNCT_1:def 3;
then
(f /. n) `1 in rng (Incr (X_axis f))
by SEQ_4:def 21;
then consider i being Nat such that
A4:
i in dom (Incr (X_axis f))
and
A5:
(Incr (X_axis f)) . i = (f /. n) `1
by FINSEQ_2:10;
A6:
n in dom (Y_axis f)
by A1, Lm2;
then
(Y_axis f) . n = (f /. n) `2
by GOBOARD1:def 2;
then
(f /. n) `2 in rng (Y_axis f)
by A6, FUNCT_1:def 3;
then
(f /. n) `2 in rng (Incr (Y_axis f))
by SEQ_4:def 21;
then consider j being Nat such that
A7:
j in dom (Incr (Y_axis f))
and
A8:
(Incr (Y_axis f)) . j = (f /. n) `2
by FINSEQ_2:10;
reconsider i = i, j = j as Nat ;
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) )
i in Seg (len (Incr (X_axis f)))
by A4, FINSEQ_1:def 3;
then
i in Seg (len (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))))
by GOBOARD2:def 1;
then A9:
i in dom (GoB f)
by A2, FINSEQ_1:def 3;
j in Seg (len (Incr (Y_axis f)))
by A7, FINSEQ_1:def 3;
then
j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))))
by GOBOARD2:def 1;
then
[i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):]
by A2, A9, ZFMISC_1:87;
hence A10:
[i,j] in Indices (GoB f)
by MATRIX_0:def 4; f /. n = (GoB f) * (i,j)
thus f /. n =
|[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]|
by A5, A8, EUCLID:53
.=
(GoB f) * (i,j)
by A2, A10, GOBOARD2:def 1
; verum