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