let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st 1 <= i & i <= len (GoB f) holds

ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

let i be Nat; :: thesis: ( 1 <= i & i <= len (GoB f) implies ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )

assume that

A1: 1 <= i and

A2: i <= len (GoB f) ; :: thesis: ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

A3: i in dom (GoB f) by A1, A2, FINSEQ_3:25;

A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def 2;

then len (Incr (X_axis f)) = len (GoB f) by GOBOARD2:def 1;

then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25;

then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def 3;

then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def 21;

then consider k being Nat such that

A5: k in dom (X_axis f) and

A6: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;

A7: len (X_axis f) = len f by GOBOARD1:def 1

.= len (Y_axis f) by GOBOARD1:def 2 ;

then dom (X_axis f) = dom (Y_axis f) by FINSEQ_3:29;

then (Y_axis f) . k in rng (Y_axis f) by A5, FUNCT_1:def 3;

then (Y_axis f) . k in rng (Incr (Y_axis f)) by SEQ_4:def 21;

then consider j being Nat such that

A8: j in dom (Incr (Y_axis f)) and

A9: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;

reconsider k = k, j = j as Nat ;

A10: (X_axis f) . k = (f /. k) `1 by A5, GOBOARD1:def 1;

take k ; :: thesis: ex j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

take j ; :: thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

len (X_axis f) = len f by GOBOARD1:def 1;

hence k in dom f by A5, FINSEQ_3:29; :: thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

j in Seg (len (Incr (Y_axis f))) by A8, 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 A4, A3, ZFMISC_1:87;

hence A11: [i,j] in Indices (GoB f) by MATRIX_0:def 4; :: thesis: f /. k = (GoB f) * (i,j)

dom (X_axis f) = dom (Y_axis f) by A7, FINSEQ_3:29;

then (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def 2;

hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53

.= (GoB f) * (i,j) by A4, A11, GOBOARD2:def 1 ;

:: thesis: verum

ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

let i be Nat; :: thesis: ( 1 <= i & i <= len (GoB f) implies ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )

assume that

A1: 1 <= i and

A2: i <= len (GoB f) ; :: thesis: ex k, j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

A3: i in dom (GoB f) by A1, A2, FINSEQ_3:25;

A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def 2;

then len (Incr (X_axis f)) = len (GoB f) by GOBOARD2:def 1;

then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25;

then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def 3;

then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def 21;

then consider k being Nat such that

A5: k in dom (X_axis f) and

A6: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;

A7: len (X_axis f) = len f by GOBOARD1:def 1

.= len (Y_axis f) by GOBOARD1:def 2 ;

then dom (X_axis f) = dom (Y_axis f) by FINSEQ_3:29;

then (Y_axis f) . k in rng (Y_axis f) by A5, FUNCT_1:def 3;

then (Y_axis f) . k in rng (Incr (Y_axis f)) by SEQ_4:def 21;

then consider j being Nat such that

A8: j in dom (Incr (Y_axis f)) and

A9: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;

reconsider k = k, j = j as Nat ;

A10: (X_axis f) . k = (f /. k) `1 by A5, GOBOARD1:def 1;

take k ; :: thesis: ex j being Nat st

( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

take j ; :: thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

len (X_axis f) = len f by GOBOARD1:def 1;

hence k in dom f by A5, FINSEQ_3:29; :: thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

j in Seg (len (Incr (Y_axis f))) by A8, 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 A4, A3, ZFMISC_1:87;

hence A11: [i,j] in Indices (GoB f) by MATRIX_0:def 4; :: thesis: f /. k = (GoB f) * (i,j)

dom (X_axis f) = dom (Y_axis f) by A7, FINSEQ_3:29;

then (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def 2;

hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53

.= (GoB f) * (i,j) by A4, A11, GOBOARD2:def 1 ;

:: thesis: verum