let f be non empty FinSequence of (TOP-REAL 2); 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; ( 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
; ( 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 )
; ( 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 )
; ( 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 )
; ( 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 )
; 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; verum