let f be non empty FinSequence of (TOP-REAL 2); for i, j being Nat st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
let i, j be Nat; ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) )
assume that
A1:
1 <= i
and
A2:
i <= len (GoB f)
and
A3:
1 <= j
and
A4:
j <= width (GoB f)
; ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
A5:
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 A3, A4, FINSEQ_3:25;
then
j in Seg (len (Incr (Y_axis f)))
by FINSEQ_1:def 3;
then A6:
j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))))
by GOBOARD2:def 1;
len (Incr (Y_axis f)) = width (GoB f)
by A5, GOBOARD2:def 1;
then
j in dom (Incr (Y_axis f))
by A3, A4, 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
A7:
k in dom (Y_axis f)
and
A8:
(Y_axis f) . k = (Incr (Y_axis f)) . j
by FINSEQ_2:10;
reconsider k = k as Nat ;
take
k
; ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
len (Y_axis f) = len f
by GOBOARD1:def 2;
hence
k in dom f
by A7, FINSEQ_3:29; ( [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
i in dom (GoB f)
by A1, A2, FINSEQ_3:25;
then
[i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):]
by A5, A6, ZFMISC_1:87;
hence
[i,j] in Indices (GoB f)
by MATRIX_0:def 4; (f /. k) `2 = ((GoB f) * (i,j)) `2
then A9:
(GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]|
by A5, GOBOARD2:def 1;
thus (f /. k) `2 =
(Incr (Y_axis f)) . j
by A7, A8, GOBOARD1:def 2
.=
((GoB f) * (i,j)) `2
by A9, EUCLID:52
; verum