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

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