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 Element of NAT st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Element of NAT st
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * (len G),i in rng f ) & ex i being Element of 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 Element of NAT st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Element of NAT st
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * (len G),i in rng f ) & ex i being Element of 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 Element of NAT holds
( not [1,i] in Indices G or not G * 1,i in rng f ) or for i being Element of NAT holds
( not [i,1] in Indices G or not G * i,1 in rng f ) or for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * (len G),i in rng f ) or for i being Element of 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 Element of NAT such that A2: [1,i1] in Indices G and
A3: G * 1,i1 in rng f ; :: thesis: ( for i being Element of NAT holds
( not [i,1] in Indices G or not G * i,1 in rng f ) or for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * (len G),i in rng f ) or for i being Element of 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 Element of NAT such that A4: [i2,1] in Indices G and
A5: G * i2,1 in rng f ; :: thesis: ( for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * (len G),i in rng f ) or for i being Element of 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 Element of NAT such that A6: [(len G),i3] in Indices G and
A7: G * (len G),i3 in rng f ; :: thesis: ( for i being Element of 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 Element of NAT such that A8: [i4,(width G)] in Indices G and
A9: G * i4,(width G) in rng f ; :: thesis: G = GoB f
A10: proj1 .: (rng f) = proj1 .: (Values G) by A1, A2, A3, A6, A7, Th36;
proj2 .: (rng f) = proj2 .: (Values G) by A1, A4, A5, A8, A9, Th37;
hence G = GoB f by A10, Th39; :: thesis: verum