let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
G = GoB f
let G be Go-board; :: thesis: ( f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) implies G = GoB f )
assume A1: f is_sequence_on G ; :: thesis: ( for i being Nat holds
( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Nat holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Nat holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Nat holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i1 being Nat such that A2: ( [1,i1] in Indices G & G * (1,i1) in rng f ) ; :: thesis: ( for i being Nat holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Nat holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Nat holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i2 being Nat such that A3: ( [i2,1] in Indices G & G * (i2,1) in rng f ) ; :: thesis: ( for i being Nat holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Nat holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i3 being Nat such that A4: ( [(len G),i3] in Indices G & G * ((len G),i3) in rng f ) ; :: thesis: ( for i being Nat holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i4 being Nat such that A5: ( [i4,(width G)] in Indices G & G * (i4,(width G)) in rng f ) ; :: thesis: G = GoB f
A6: proj2 .: (rng f) = proj2 .: (Values G) by A1, A3, A5, Th31;
proj1 .: (rng f) = proj1 .: (Values G) by A1, A2, A4, Th30;
hence G = GoB f by A6, Th33; :: thesis: verum