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

ex k being Nat st

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

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

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

assume that

A1: 1 <= i and

A2: i <= len (GoB f) and

A3: 1 <= j and

A4: j <= width (GoB f) ; :: thesis: ex k being Nat st

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

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

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

then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;

then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def 3;

then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def 1;

len (Incr (Y_axis f)) = width (GoB f) by A5, GOBOARD2:def 1;

then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;

then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def 3;

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

then consider k being Nat such that

A7: k in dom (Y_axis f) and

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

reconsider k = k as Nat ;

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

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

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

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

then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87;

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

then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def 1;

thus (f /. k) `2 = (Incr (Y_axis f)) . j by A7, A8, GOBOARD1:def 2

.= ((GoB f) * (i,j)) `2 by A9, EUCLID:52 ; :: thesis: verum

ex k being Nat st

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

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

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

assume that

A1: 1 <= i and

A2: i <= len (GoB f) and

A3: 1 <= j and

A4: j <= width (GoB f) ; :: thesis: ex k being Nat st

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

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

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

then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;

then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def 3;

then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def 1;

len (Incr (Y_axis f)) = width (GoB f) by A5, GOBOARD2:def 1;

then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25;

then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def 3;

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

then consider k being Nat such that

A7: k in dom (Y_axis f) and

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

reconsider k = k as Nat ;

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

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

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

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

then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87;

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

then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def 1;

thus (f /. k) `2 = (Incr (Y_axis f)) . j by A7, A8, GOBOARD1:def 2

.= ((GoB f) * (i,j)) `2 by A9, EUCLID:52 ; :: thesis: verum