let
X
be
RealUnitarySpace
;
:: thesis:
X
*'
=
(
RUSp2RNSp
X
)
*'
set
Y
=
RUSp2RNSp
X
;
the
carrier
of
(
X
*'
)
=
the
carrier
of
(
(
RUSp2RNSp
X
)
*'
)
by
LM10A
;
hence
X
*'
=
(
RUSp2RNSp
X
)
*'
;
:: thesis:
verum