let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j )
let n be Element of NAT ; :: thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j ) )
assume A1: n in dom f ; :: thesis: ex i, j being Element of 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 3;
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 3;
then (f /. n) `1 in rng (X_axis f) by A3, FUNCT_1:def 5;
then (f /. n) `1 in rng (Incr (X_axis f)) by SEQ_4:def 25;
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:11;
A6: n in dom (Y_axis f) by A1, Lm2;
then (Y_axis f) . n = (f /. n) `2 by GOBOARD1:def 4;
then (f /. n) `2 in rng (Y_axis f) by A6, FUNCT_1:def 5;
then (f /. n) `2 in rng (Incr (Y_axis f)) by SEQ_4:def 25;
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:11;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j )
take j ; :: thesis: ( [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:106;
hence A10: [i,j] in Indices (GoB f) by MATRIX_1:def 5; :: thesis: f /. n = (GoB f) * i,j
thus f /. n = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, A8, EUCLID:57
.= (GoB f) * i,j by A2, A10, GOBOARD2:def 1 ; :: thesis: verum