let
x
be
Vector
of
[:
G
,
F
:]
;
:: according to
VECTSP_1:def 16
:: thesis:
(
1.
K
)
*
x
=
x
consider
x1
being
Vector
of
G
,
x2
being
Vector
of
F
such that
A1
:
x
=
[
x1
,
x2
]
by
SUBSET_1:43
;
(
(
1.
K
)
*
x1
=
x1
&
(
1.
K
)
*
x2
=
x2
)
by
VECTSP_1:def 17
;
hence
(
1.
K
)
*
x
=
x
by
A1
,
YDef2
;
:: thesis:
verum