let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) )
set x = X_axis f;
set y = Y_axis f;
( len (Incr (X_axis f)) = card (rng (X_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by SEQ_4:def 21;
hence ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) by Def1; :: thesis: verum