let f be non empty FinSequence of (TOP-REAL 2); :: thesis:
let j be Nat; :: thesis:
assume that
A1: 1 <= j and
A2: j <= width (GoB f) ; :: thesis:
A3: j in Seg (width (GoB f)) by A1, A2, FINSEQ_1:1;
A4: 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 A1, A2, 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
A5: k in dom (Y_axis f) and
A6: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10;
A7: len (X_axis f) = len f by GOBOARD1:def 1
.= len (Y_axis f) by GOBOARD1:def 2 ;
then k in dom (X_axis f) by A5, FINSEQ_3:29;
then (X_axis f) . k in rng (X_axis f) by FUNCT_1:def 3;
then (X_axis f) . k in rng (Incr (X_axis f)) by SEQ_4:def 21;
then consider i being Nat such that
A8: i in dom (Incr (X_axis f)) and
A9: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10;
reconsider k = k, i = i as Nat ;
k in dom (X_axis f) by A5, A7, FINSEQ_3:29;
then A10: (X_axis f) . k = (f /. k) `1 by GOBOARD1:def 1;
take k ; :: thesis:
take i ; :: thesis:
len (Y_axis f) = len f by GOBOARD1:def 2;
hence k in dom f by A5, FINSEQ_3:29; :: thesis:
len (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) = len (Incr (X_axis f)) by GOBOARD2:def 1;
then i in dom (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A8, FINSEQ_3:29;
then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A4, A3, ZFMISC_1:87;
hence A11: [i,j] in Indices (GoB f) by MATRIX_0:def 4; :: thesis:
(Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def 2;
hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53
.= (GoB f) * (i,j) by A4, A11, GOBOARD2:def 1 ;
:: thesis: