let h be non constant standard special_circular_sequence; :: thesis: ( 1 <= i_n_e h & i_n_e h <= width (GoB h) & 1 <= i_s_e h & i_s_e h <= width (GoB h) & 1 <= i_n_w h & i_n_w h <= width (GoB h) & 1 <= i_s_w h & i_s_w h <= width (GoB h) )
A1: [(len (GoB h)),(i_s_e h)] in Indices (GoB h) by Def3;
A2: [1,(i_n_w h)] in Indices (GoB h) by Def2;
A3: [1,(i_s_w h)] in Indices (GoB h) by Def1;
[(len (GoB h)),(i_n_e h)] in Indices (GoB h) by Def4;
hence ( 1 <= i_n_e h & i_n_e h <= width (GoB h) & 1 <= i_s_e h & i_s_e h <= width (GoB h) & 1 <= i_n_w h & i_n_w h <= width (GoB h) & 1 <= i_s_w h & i_s_w h <= width (GoB h) ) by A1, A2, A3, MATRIX_0:32; :: thesis: verum