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