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 )
set x = X_axis f;
set y = Y_axis f;
A1: ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) & GoB f = GoB (Incr (X_axis f)),(Incr (Y_axis f)) & X_axis f <> {} & Y_axis f <> {} ) by Th24;
A2: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & Incr (X_axis f) <> {} & Incr (Y_axis f) <> {} ) by MATRIX_1:def 5;
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 A3: 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 )
A4: ( dom f = Seg (len f) & dom (X_axis f) = Seg (len (X_axis f)) & dom (Y_axis f) = Seg (len (Y_axis f)) & rng f c= the carrier of (TOP-REAL 2) ) by FINSEQ_1:def 3, FINSEQ_1:def 4;
reconsider p = f /. n as Point of (TOP-REAL 2) ;
( len (X_axis f) = len f & len (Y_axis f) = len f ) by GOBOARD1:def 3, GOBOARD1:def 4;
then A5: ( (X_axis f) . n = p `1 & (Y_axis f) . n = p `2 & (X_axis f) . n in rng (X_axis f) & (Y_axis f) . n in rng (Y_axis f) ) by A3, A4, FUNCT_1:def 5, GOBOARD1:def 3, GOBOARD1:def 4;
A6: ( rng (Incr (X_axis f)) = rng (X_axis f) & rng (Incr (Y_axis f)) = rng (Y_axis f) & len (Incr (X_axis f)) = card (rng (X_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Def2;
then consider i being Nat such that
A7: ( i in dom (Incr (X_axis f)) & (Incr (X_axis f)) . i = p `1 ) by A5, FINSEQ_2:11;
consider j being Nat such that
A8: ( j in dom (Incr (Y_axis f)) & (Incr (Y_axis f)) . j = p `2 ) by A5, A6, 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 )
( dom (GoB f) = dom (Incr (X_axis f)) & Seg (width (GoB f)) = dom (Incr (Y_axis f)) ) by A1, A6, FINSEQ_1:def 3, FINSEQ_3:31;
hence [i,j] in Indices (GoB f) by A2, A7, A8, ZFMISC_1:106; :: thesis: f /. n = (GoB f) * i,j
then ( (GoB f) * i,j = |[(p `1 ),(p `2 )]| & p = |[(p `1 ),(p `2 )]| ) by A7, A8, Def1, EUCLID:57;
hence f /. n = (GoB f) * i,j ; :: thesis: verum