let f be non empty FinSequence of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex j being 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) )

( 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; :: thesis: 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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex j being 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) )

( 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; :: thesis: 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; :: thesis: verum