consider
A
being
finite
Subset
of
V
such that
A1
:
A
is
Basis
of
V
by
Def3
;
consider
n
being
Nat
such that
A2
:
n
=
card
A
;
for
I
being
Basis
of
V
holds
card
I
=
n
by
A1
,
A2
,
Th36
;
hence
ex
b
_{1}
being
Nat
st
for
I
being
Basis
of
V
holds
b
_{1}
=
card
I
;
:: thesis:
verum