let f be non empty FinSequence of (); :: thesis: for j being Nat st 1 <= j & j <= width (GoB f) holds
ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

let j be Nat; :: thesis: ( 1 <= j & j <= width (GoB f) implies ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) )

assume that
A1: 1 <= j and
A2: j <= width (GoB f) ; :: thesis: ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

A3: j in Seg (width (GoB f)) by ;
A4: 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 (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
A5: k in dom () and
A6: (Y_axis f) . k = (Incr ()) . j by FINSEQ_2:10;
A7: len () = len f by GOBOARD1:def 1
.= len () by GOBOARD1:def 2 ;
then k in dom () by ;
then (X_axis f) . k in rng () by FUNCT_1:def 3;
then (X_axis f) . k in rng (Incr ()) by SEQ_4:def 21;
then consider i being Nat such that
A8: i in dom (Incr ()) and
A9: (X_axis f) . k = (Incr ()) . i by FINSEQ_2:10;
reconsider k = k, i = i as Nat ;
k in dom () by ;
then A10: (X_axis f) . k = (f /. k) `1 by GOBOARD1:def 1;
take k ; :: thesis: ex i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )

take i ; :: thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
len () = len f by GOBOARD1:def 2;
hence k in dom f by ; :: thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
len (GoB ((Incr ()),(Incr ()))) = len (Incr ()) by GOBOARD2:def 1;
then i in dom (GoB ((Incr ()),(Incr ()))) by ;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by ;
hence A11: [i,j] in Indices (GoB f) by MATRIX_0:def 4; :: thesis: f /. k = (GoB f) * (i,j)
(Y_axis f) . k = (f /. k) `2 by ;
hence f /. k = |[((Incr ()) . i),((Incr ()) . j)]| by
.= (GoB f) * (i,j) by ;
:: thesis: verum