:: deftheorem Def1 defines v_strip GOBOARD5:def 1 :
for G being Matrix of (TOP-REAL 2)
for i being Nat holds
( ( 1 <= i & i < len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) & ( i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ) );