let f be non empty FinSequence of (); :: thesis: for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

set x = X_axis f;
set y = Y_axis f;
let n be Nat; :: thesis: ( n in dom f implies ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) )

assume A1: n in dom f ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

A2: rng (Incr ()) = rng () by SEQ_4:def 21;
reconsider p = f /. n as Point of () ;
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
( dom () = Seg (len ()) & len () = len f ) by ;
then ( (Y_axis f) . n = p `2 & () . n in rng () ) by ;
then consider j being Nat such that
A4: j in dom (Incr ()) and
A5: (Incr ()) . j = p `2 by ;
A6: rng (Incr ()) = rng () by SEQ_4:def 21;
( dom () = Seg (len ()) & len () = len f ) by ;
then ( (X_axis f) . n = p `1 & () . n in rng () ) by ;
then consider i being Nat such that
A7: i in dom (Incr ()) and
A8: (Incr ()) . i = p `1 by ;
( width (GoB f) = card (rng ()) & len (Incr ()) = card (rng ()) ) by ;
then A9: Seg (width (GoB f)) = dom (Incr ()) by FINSEQ_1:def 3;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 12;
take i ; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

take j ; :: thesis: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
( len (GoB f) = card (rng ()) & len (Incr ()) = card (rng ()) ) by ;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (GoB f) = dom (Incr ()) ) by ;
hence [i,j] in Indices (GoB f) by ; :: thesis: f /. n = (GoB f) * (i,j)
then (GoB f) * (i,j) = |[(p `1),(p `2)]| by A8, A5, Def1;
hence f /. n = (GoB f) * (i,j) by EUCLID:53; :: thesis: verum