let f be non empty FinSequence of (); :: 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 ()),(Incr ())) by GOBOARD2:def 2;
then len (Incr ()) = width (GoB f) by GOBOARD2:def 1;
then j in dom (Incr ()) by ;
then j in Seg (len (Incr ())) by FINSEQ_1:def 3;
then A6: j in Seg (width (GoB ((Incr ()),(Incr ())))) by GOBOARD2:def 1;
len (Incr ()) = width (GoB f) by ;
then j in dom (Incr ()) by ;
then (Incr ()) . j in rng (Incr ()) by FUNCT_1:def 3;
then (Incr ()) . j in rng () by SEQ_4:def 21;
then consider k being Nat such that
A7: k in dom () and
A8: (Y_axis f) . k = (Incr ()) . 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 () = len f by GOBOARD1:def 2;
hence k in dom f by ; :: thesis: ( [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
i in dom (GoB f) by ;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by ;
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 ()) . i),((Incr ()) . j)]| by ;
thus (f /. k) `2 = (Incr ()) . j by
.= ((GoB f) * (i,j)) `2 by ; :: thesis: verum