:: RUSUB_5 semantic presentation
begin
definition
let
V
be ( ( non
empty
) ( non
empty
)
RLSStruct
) ;
let
M
,
N
be ( (
Affine
) (
Affine
)
Subset
of ) ;
pred
M
is_parallel_to
N
means
:: RUSUB_5:def 1
ex
v
being ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) st
M
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) )
=
N
: ( (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) ) (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) )
Element
of
K10
(
K11
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
+
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: RUSUB_5:1
for
V
being ( ( non
empty
right_zeroed
) ( non
empty
right_zeroed
)
RLSStruct
)
for
M
being ( (
Affine
) (
Affine
)
Subset
of ) holds
M
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
M
: ( (
Affine
) (
Affine
)
Subset
of ) ;
theorem
:: RUSUB_5:2
for
V
being ( ( non
empty
right_complementable
add-associative
right_zeroed
) ( non
empty
right_complementable
add-associative
right_zeroed
)
RLSStruct
)
for
M
,
N
being ( (
Affine
) (
Affine
)
Subset
of ) st
M
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
N
: ( (
Affine
) (
Affine
)
Subset
of ) holds
N
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
M
: ( (
Affine
) (
Affine
)
Subset
of ) ;
theorem
:: RUSUB_5:3
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
RLSStruct
)
for
M
,
L
,
N
being ( (
Affine
) (
Affine
)
Subset
of ) st
M
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
L
: ( (
Affine
) (
Affine
)
Subset
of ) &
L
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
N
: ( (
Affine
) (
Affine
)
Subset
of ) holds
M
: ( (
Affine
) (
Affine
)
Subset
of )
is_parallel_to
N
: ( (
Affine
) (
Affine
)
Subset
of ) ;
definition
let
V
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
let
M
,
N
be ( ( ) ( )
Subset
of ) ;
func
M
-
N
->
( ( ) ( )
Subset
of )
equals
:: RUSUB_5:def 2
{
(
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
-
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
) ) where
u
,
v
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) : (
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) ) &
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) ) (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) )
Element
of
K10
(
K11
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
;
end;
theorem
:: RUSUB_5:4
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
,
N
being ( (
Affine
) (
Affine
)
Subset
of ) holds
M
: ( (
Affine
) (
Affine
)
Subset
of )
-
N
: ( (
Affine
) (
Affine
)
Subset
of ) : ( ( ) ( )
Subset
of ) is
Affine
;
theorem
:: RUSUB_5:5
for
V
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
M
,
N
being ( ( ) ( )
Subset
of ) st (
M
: ( ( ) ( )
Subset
of ) is
empty
or
N
: ( ( ) ( )
Subset
of ) is
empty
) holds
M
: ( ( ) ( )
Subset
of )
+
N
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: RUSUB_5:6
for
V
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
M
,
N
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds not
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
+
N
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: RUSUB_5:7
for
V
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
M
,
N
being ( ( ) ( )
Subset
of ) st (
M
: ( ( ) ( )
Subset
of ) is
empty
or
N
: ( ( ) ( )
Subset
of ) is
empty
) holds
M
: ( ( ) ( )
Subset
of )
-
N
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) is
empty
;
theorem
:: RUSUB_5:8
for
V
being ( ( non
empty
) ( non
empty
)
addLoopStr
)
for
M
,
N
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds not
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
-
N
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) is
empty
;
theorem
:: RUSUB_5:9
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
)
for
M
,
N
being ( ( ) ( )
Subset
of )
for
v
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
M
: ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( )
Subset
of )
+
{
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff
M
: ( ( ) ( )
Subset
of )
-
{
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: RUSUB_5:10
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
)
for
M
,
N
being ( ( ) ( )
Subset
of )
for
v
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( )
Subset
of ) holds
M
: ( ( ) ( )
Subset
of )
+
{
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
M
: ( ( ) ( )
Subset
of )
+
N
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RUSUB_5:11
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
)
for
M
,
N
being ( ( ) ( )
Subset
of )
for
v
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( )
Subset
of ) holds
M
: ( ( ) ( )
Subset
of )
-
{
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V125
() )
addLoopStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
M
: ( ( ) ( )
Subset
of )
-
N
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RUSUB_5:12
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
-
M
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RUSUB_5:13
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) is
Subspace-like
&
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
+
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) ;
theorem
:: RUSUB_5:14
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
,
N1
,
N2
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) st
N1
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) is
Subspace-like
&
N2
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) is
Subspace-like
&
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
is_parallel_to
N1
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) &
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
is_parallel_to
N2
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
N1
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
=
N2
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) ;
theorem
:: RUSUB_5:15
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RUSUB_5:16
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
ex
N
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) st
(
N
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
=
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) &
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
is_parallel_to
N
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) &
N
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) is
Subspace-like
) ;
theorem
:: RUSUB_5:17
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
for
u
,
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) &
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RUSUB_5:18
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) : ( ( ) ( )
Subset
of )
=
union
{
(
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) where
v
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) :
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
}
: ( ( ) ( )
set
) ;
theorem
:: RUSUB_5:19
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) holds
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
union
{
(
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) :
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
}
: ( ( ) ( )
set
) ;
theorem
:: RUSUB_5:20
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
() )
RealLinearSpace
)
for
M
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) ex
L
being ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) st
(
L
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
=
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
-
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) : ( ( ) ( )
Subset
of ) &
L
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) is
Subspace-like
&
M
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of )
is_parallel_to
L
: ( ( non
empty
Affine
) ( non
empty
Affine
)
Subset
of ) ) ;
begin
definition
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
let
W
be ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
func
Ort_Comp
W
->
( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
V
: ( ( ) ( )
UNITSTR
) )
means
:: RUSUB_5:def 3
the
carrier
of
it
: ( (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) ) (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) )
Element
of
K10
(
K11
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
v
is ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) : for
w
being ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) st
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
W
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) ) holds
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
are_orthogonal
}
;
end;
definition
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
let
M
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
func
Ort_Comp
M
->
( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
V
: ( ( ) ( )
UNITSTR
) )
means
:: RUSUB_5:def 4
the
carrier
of
it
: ( (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) ) (
V31
()
V40
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) )
Element
of
K10
(
K11
(
K11
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
v
is ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) : for
w
being ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) st
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) ) holds
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
are_orthogonal
}
;
end;
theorem
:: RUSUB_5:21
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
W
being ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) holds
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
in
Ort_Comp
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:22
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) holds
Ort_Comp
(
(0).
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
=
(Omega).
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:23
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) holds
Ort_Comp
(
(Omega).
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
=
(0).
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:24
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
W
being ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
<>
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) &
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) holds
not
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Ort_Comp
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:25
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
the
carrier
of
(
Ort_Comp
(
Ort_Comp
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: RUSUB_5:26
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
,
N
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
N
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
the
carrier
of
(
Ort_Comp
N
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( ( ) ( non
empty
)
set
)
c=
the
carrier
of
(
Ort_Comp
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: RUSUB_5:27
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
W
being ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
for
M
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( ( ) ( non
empty
)
set
) holds
Ort_Comp
M
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
=
Ort_Comp
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:28
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
Ort_Comp
M
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
=
Ort_Comp
(
Ort_Comp
(
Ort_Comp
M
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) )
)
: ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( (
strict
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
strict
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) ;
theorem
:: RUSUB_5:29
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
x
,
y
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
||.
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
=
(
(
||.
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
2 : ( ( ) ( non
empty
natural
V14
()
real
ext-real
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
||.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) &
||.
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
-
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
=
(
(
||.
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
-
(
2 : ( ( ) ( non
empty
natural
V14
()
real
ext-real
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
||.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) ) ;
theorem
:: RUSUB_5:30
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
x
,
y
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
are_orthogonal
holds
||.
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
=
(
||.
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
||.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) ;
theorem
:: RUSUB_5:31
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
x
,
y
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
||.
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
||.
(
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
-
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
=
(
2 : ( ( ) ( non
empty
natural
V14
()
real
ext-real
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*
(
||.
x
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
+
(
2 : ( ( ) ( non
empty
natural
V14
()
real
ext-real
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*
(
||.
y
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.||
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
^2
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
)
: ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) ;
theorem
:: RUSUB_5:32
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ex
W
being ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) st the
carrier
of
W
: ( ( ) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
Subspace
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) : ( ( ) ( non
empty
)
set
)
=
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) :
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V14
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) )
=
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
;
begin
definition
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
func
Family_open_set
V
->
( ( ) ( )
Subset-Family
of )
means
:: RUSUB_5:def 5
for
M
being ( ( ) ( )
Subset
of ) holds
(
M
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) ) iff for
x
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( ) ( )
Subset
of ) holds
ex
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
Ball
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
M
: ( ( ) ( )
Subset
of ) ) );
end;
theorem
:: RUSUB_5:33
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r
,
p
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
<=
p
: ( ( ) (
V14
()
real
ext-real
)
Real
) holds
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
p
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RUSUB_5:34
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ex
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RUSUB_5:35
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
,
u
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
u
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
ex
p
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
p
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
Ball
(
u
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
p
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RUSUB_5:36
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
u
,
v
,
w
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r
,
p
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
(
Ball
(
u
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
(
Ball
(
w
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
p
: ( ( ) (
V14
()
real
ext-real
)
Real
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
ex
q
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
q
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Ball
(
u
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
q
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Ball
(
w
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
p
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RUSUB_5:37
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) holds
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: RUSUB_5:38
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) holds the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: RUSUB_5:39
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
,
N
being ( ( ) ( )
Subset
of ) st
M
: ( ( ) ( )
Subset
of )
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) &
N
: ( ( ) ( )
Subset
of )
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) holds
M
: ( ( ) ( )
Subset
of )
/\
N
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: RUSUB_5:40
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
A
being ( ( ) ( )
Subset-Family
of ) st
A
: ( ( ) ( )
Subset-Family
of )
c=
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) holds
union
A
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: RUSUB_5:41
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) holds
TopStruct
(# the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ,
(
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) ( )
Subset-Family
of ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) is ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
definition
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
func
TopUnitSpace
V
->
( ( ) ( )
TopStruct
)
equals
:: RUSUB_5:def 6
TopStruct
(# the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
) ,
(
Family_open_set
V
: ( ( ) ( )
UNITSTR
)
)
: ( ( ) ( )
Subset-Family
of ) #) : ( (
strict
) (
strict
)
TopStruct
) ;
end;
registration
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
cluster
TopUnitSpace
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( )
TopStruct
)
->
TopSpace-like
;
end;
registration
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ;
cluster
TopUnitSpace
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) (
TopSpace-like
)
TopStruct
)
->
non
empty
;
end;
theorem
:: RUSUB_5:42
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of ) st
M
: ( ( ) ( )
Subset
of )
=
[#]
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
non
proper
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
(
M
: ( ( ) ( )
Subset
of ) is
open
&
M
: ( ( ) ( )
Subset
of ) is
closed
) ;
theorem
:: RUSUB_5:43
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of ) st
M
: ( ( ) ( )
Subset
of )
=
{}
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) (
empty
proper
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
(
M
: ( ( ) ( )
Subset
of ) is
open
&
M
: ( ( ) ( )
Subset
of ) is
closed
) ;
theorem
:: RUSUB_5:44
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
=
{
(
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
<>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
Sphere
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: RUSUB_5:45
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
<>
{
(
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
not
Sphere
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: RUSUB_5:46
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
=
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
Ball
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: RUSUB_5:47
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
=
{
(
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
Ball
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{
(
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RUSUB_5:48
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
<>
{
(
0.
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) (
V59
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
(
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
<>
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) &
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Ball
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RUSUB_5:49
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) holds
( the
carrier
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
)
=
the
carrier
of
(
TopUnitSpace
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) & the
topology
of
(
TopUnitSpace
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
(
TopUnitSpace
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
)
: ( ( ) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
Family_open_set
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( )
Subset-Family
of ) ) ;
theorem
:: RUSUB_5:50
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
)
for
v
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
M
: ( ( ) ( )
Subset
of )
=
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
M
: ( ( ) ( )
Subset
of ) is
open
;
theorem
:: RUSUB_5:51
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of ) holds
(
M
: ( ( ) ( )
Subset
of ) is
open
iff for
v
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
M
: ( ( ) ( )
Subset
of ) holds
ex
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
r
: ( ( ) (
V14
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
natural
V14
()
real
ext-real
non
positive
non
negative
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
NAT
: ( ( ) (
V19
()
V20
()
V21
()
V22
()
V23
()
V24
()
V25
() )
Element
of
K10
(
REAL
: ( ( ) (
V19
()
V20
()
V21
()
V25
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
Ball
(
v
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
M
: ( ( ) ( )
Subset
of ) ) ) ;
theorem
:: RUSUB_5:52
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
v1
,
v2
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r1
,
r2
being ( ( ) (
V14
()
real
ext-real
)
Real
) ex
u
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ex
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
(
Ball
(
v1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r1
: ( ( ) (
V14
()
real
ext-real
)
Real
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
Ball
(
v2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r2
: ( ( ) (
V14
()
real
ext-real
)
Real
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Ball
(
u
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RUSUB_5:53
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
M
: ( ( ) ( )
Subset
of )
=
cl_Ball
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
M
: ( ( ) ( )
Subset
of ) is
closed
;
theorem
:: RUSUB_5:54
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
)
for
M
being ( ( ) ( )
Subset
of )
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
r
being ( ( ) (
V14
()
real
ext-real
)
Real
) st
M
: ( ( ) ( )
Subset
of )
=
Sphere
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
r
: ( ( ) (
V14
()
real
ext-real
)
Real
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
RealUnitarySpace-like
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V125
()
RealUnitarySpace-like
)
RealUnitarySpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
M
: ( ( ) ( )
Subset
of ) is
closed
;