let i, j be Element of NAT ; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Element of NAT st
( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies ex k being Element of NAT st
( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) )
assume that
A1: ( 1 <= i & i <= len (GoB f) ) and
A2: ( 1 <= j & j <= width (GoB f) ) ; :: thesis: ex k being Element of NAT st
( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
A3: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def 3;
then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def 1;
then j in dom (Incr (Y_axis f)) by A2, FINSEQ_3:27;
then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def 5;
then (Incr (Y_axis f)) . j in rng (Y_axis f) by SEQ_4:def 25;
then consider k being Nat such that
A4: k in dom (Y_axis f) and
A5: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:11;
[i,j] in Indices (GoB f) by A1, A2, MATRIX_1:37;
then A6: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A3, GOBOARD2:def 1;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
take k ; :: thesis: ( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
len (Y_axis f) = len f by GOBOARD1:def 4;
hence k in dom f by A4, FINSEQ_3:31; :: thesis: (f /. k) `2 = ((GoB f) * (i,j)) `2
thus (f /. k) `2 = (Incr (Y_axis f)) . j by A4, A5, GOBOARD1:def 4
.= ((GoB f) * (i,j)) `2 by A6, EUCLID:56 ; :: thesis: verum