let G be V9() Matrix of (TOP-REAL 2); ( G is X_equal-in-line implies v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } )
0 <> width G
by MATRIX_0:def 10;
then A1:
1 <= width G
by NAT_1:14;
assume
G is X_equal-in-line
; v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r }
hence
v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r }
by A1, GOBOARD5:9; verum