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