now
:: thesis:
( not
deg
(
E
,
F
)
=

1 implies
deg
(
E
,
F
) is
natural
)
assume
A1
: not
deg
(
E
,
F
)
=

1 ;
:: thesis:
deg
(
E
,
F
) is
natural
dim
(
VecSp
(
E
,
F
)
)
is
Nat
;
hence
deg
(
E
,
F
) is
natural
by
Def6
,
A1
;
:: thesis:
verum
end;
hence
deg
(
E
,
F
) is
dimlike
;
:: thesis:
verum