:: RSSPACE semantic presentation
begin
definition
func
the_set_of_RealSequences
->
( ( non
empty
) ( non
empty
)
set
)
means
:: RSSPACE:def 1
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( ( ) ( )
UNITSTR
) iff
x
: ( ( ) ( )
set
) is ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) );
end;
definition
let
a
be ( ( ) ( )
set
) ;
assume
a
: ( ( ) ( )
set
)
in
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ;
func
seq_id
a
->
( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
equals
:: RSSPACE:def 2
a
: ( ( ) ( )
UNITSTR
) ;
end;
definition
let
a
be ( ( ) ( )
set
) ;
assume
a
: ( ( ) ( )
set
)
in
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ;
func
R_id
a
->
( ( ) (
V33
()
real
ext-real
)
Real
)
equals
:: RSSPACE:def 3
a
: ( ( ) ( )
UNITSTR
) ;
end;
definition
func
l_add
->
( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
means
:: RSSPACE:def 4
for
a
,
b
being ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) holds
it
: ( ( ) ( )
UNITSTR
)
.
(
a
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
b
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
=
(
seq_id
a
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
+
(
seq_id
b
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ;
end;
definition
func
l_mult
->
( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
means
:: RSSPACE:def 5
for
r
,
x
being ( ( ) ( )
set
) st
r
: ( ( ) ( )
set
)
in
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) &
x
: ( ( ) ( )
set
)
in
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) holds
it
: ( ( ) ( )
UNITSTR
)
.
(
r
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
(
R_id
r
: ( ( ) ( )
set
)
)
: ( ( ) (
V33
()
real
ext-real
)
Real
)
(#)
(
seq_id
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ;
end;
definition
func
Zeroseq
->
( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) )
means
:: RSSPACE:def 6
for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) holds
(
seq_id
it
: ( ( ) ( )
UNITSTR
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) ;
end;
theorem
:: RSSPACE:1
for
x
being ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) holds
seq_id
x
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
=
x
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) ;
theorem
:: RSSPACE:2
for
v
,
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
(
seq_id
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
+
(
seq_id
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: RSSPACE:3
for
r
being ( ( ) (
V33
()
real
ext-real
)
Real
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
r
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
r
: ( ( ) (
V33
()
real
ext-real
)
Real
)
(#)
(
seq_id
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ;
registration
cluster
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
RLSStruct
)
->
strict
Abelian
;
end;
theorem
:: RSSPACE:4
for
u
,
v
,
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
+
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:5
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
0.
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
)
)
: ( ( ) (
V86
(
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) ) )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:6
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ex
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
0.
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) (
V86
(
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) ) )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:7
for
a
being ( ( ) (
V33
()
real
ext-real
)
Real
)
for
v
,
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
(
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
+
(
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:8
for
a
,
b
being ( ( ) (
V33
()
real
ext-real
)
Real
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
+
b
: ( ( ) (
V33
()
real
ext-real
)
Real
)
)
: ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
(
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:9
for
a
,
b
being ( ( ) (
V33
()
real
ext-real
)
Real
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V33
()
real
ext-real
)
Real
)
)
: ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
(
b
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RSSPACE:10
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
positive
non
negative
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ;
definition
func
Linear_Space_of_RealSequences
->
( ( ) ( )
RLSStruct
)
equals
:: RSSPACE:def 7
RLSStruct
(#
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
Zeroseq
: ( ( ) ( )
Element
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_add
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) ,
l_mult
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
)
-defined
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) ,
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
Abelian
)
RLSStruct
) ;
end;
registration
cluster
Linear_Space_of_RealSequences
: ( ( ) ( )
RLSStruct
)
->
non
empty
strict
;
end;
registration
cluster
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
strict
)
RLSStruct
)
->
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
;
end;
definition
let
X
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ;
let
X1
be ( ( ) ( )
Subset
of ) ;
assume
(
X1
: ( ( ) ( )
Subset
of ) is
linearly-closed
& not
X1
: ( ( ) ( )
Subset
of ) is
empty
) ;
func
Add_
(
X1
,
X
)
->
( (
Function-like
quasi_total
) (
Relation-like
[:
X1
: ( ( ) ( )
set
) ,
X1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X1
: ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
BinOp
of
X1
: ( ( ) ( )
set
) )
equals
:: RSSPACE:def 8
the
addF
of
X
: ( ( ) ( )
set
) : ( (
Function-like
quasi_total
) (
Relation-like
[:
the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
||
X1
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
Function-like
)
set
) ;
end;
definition
let
X
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ;
let
X1
be ( ( ) ( )
Subset
of ) ;
assume
(
X1
: ( ( ) ( )
Subset
of ) is
linearly-closed
& not
X1
: ( ( ) ( )
Subset
of ) is
empty
) ;
func
Mult_
(
X1
,
X
)
->
( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
X1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X1
: ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
X1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X1
: ( ( ) ( )
set
) )
equals
:: RSSPACE:def 9
the
Mult
of
X
: ( ( ) ( )
set
) : ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
|
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
X1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( (
Function-like
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
Function-like
)
Element
of
bool
[:
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
definition
let
X
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ;
let
X1
be ( ( ) ( )
Subset
of ) ;
assume
(
X1
: ( ( ) ( )
Subset
of ) is
linearly-closed
& not
X1
: ( ( ) ( )
Subset
of ) is
empty
) ;
func
Zero_
(
X1
,
X
)
->
( ( ) ( )
Element
of
X1
: ( ( ) ( )
set
) )
equals
:: RSSPACE:def 10
0.
X
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of the
carrier
of
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: RSSPACE:11
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
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
)
for
V1
being ( ( ) ( )
Subset
of ) st
V1
: ( ( ) ( )
Subset
of ) is
linearly-closed
& not
V1
: ( ( ) ( )
Subset
of ) is
empty
holds
RLSStruct
(#
V1
: ( ( ) ( )
Subset
of ) ,
(
Zero_
(
V1
: ( ( ) ( )
Subset
of ) ,
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) )
)
: ( ( ) ( )
Element
of
b
2
: ( ( ) ( )
Subset
of ) ) ,
(
Add_
(
V1
: ( ( ) ( )
Subset
of ) ,
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
b
2
: ( ( ) ( )
Subset
of ) ,
b
2
: ( ( ) ( )
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
b
2
: ( ( ) ( )
Subset
of )
-valued
Function-like
quasi_total
)
BinOp
of
b
2
: ( ( ) ( )
Subset
of ) ) ,
(
Mult_
(
V1
: ( ( ) ( )
Subset
of ) ,
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
b
2
: ( ( ) ( )
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
b
2
: ( ( ) ( )
Subset
of )
-valued
Function-like
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
b
2
: ( ( ) ( )
Subset
of )
:]
: ( ( ) ( )
set
) ,
b
2
: ( ( ) ( )
Subset
of ) ) #) : ( (
strict
) (
strict
)
RLSStruct
) is ( ( ) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
Subspace
of
V
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ) ;
definition
func
the_set_of_l2RealSequences
->
( ( ) ( )
Subset
of )
means
:: RSSPACE:def 11
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( ( ) ( )
set
) iff (
x
: ( ( ) ( )
set
)
in
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) &
(
seq_id
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
(#)
(
seq_id
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) is
summable
) );
end;
registration
cluster
the_set_of_l2RealSequences
: ( ( ) ( )
Subset
of )
->
non
empty
linearly-closed
;
end;
theorem
:: RSSPACE:12
RLSStruct
(#
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
(
Zero_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( ( ) ( )
Element
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Add_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Mult_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) #) : ( (
strict
) ( non
empty
strict
)
RLSStruct
) is ( ( ) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
Subspace
of
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) ) ;
theorem
:: RSSPACE:13
RLSStruct
(#
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
(
Zero_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( ( ) ( )
Element
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Add_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Mult_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) #) : ( (
strict
) ( non
empty
strict
)
RLSStruct
) is ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ;
theorem
:: RSSPACE:14
( the
carrier
of
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) : ( ( ) ( non
empty
)
set
)
=
the_set_of_RealSequences
: ( ( non
empty
) ( non
empty
)
set
) & ( for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) (
V33
()
real
ext-real
)
Real
) is ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) iff
x
: ( ( ) (
V33
()
real
ext-real
)
Real
) is ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) ) ) & ( for
u
being ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
u
: ( ( ) (
V33
()
real
ext-real
)
Real
)
=
seq_id
u
: ( ( ) (
V33
()
real
ext-real
)
Real
) : ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) ) & ( for
u
,
v
being ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
u
: ( ( ) (
V33
()
real
ext-real
)
Real
)
+
v
: ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
left_complementable
right_complementable
complementable
)
Element
of the
carrier
of
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
(
seq_id
u
: ( ( ) (
V33
()
real
ext-real
)
Real
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
+
(
seq_id
v
: ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ) & ( for
r
being ( ( ) (
V33
()
real
ext-real
)
Real
)
for
u
being ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
r
: ( ( ) (
V33
()
real
ext-real
)
Real
)
*
u
: ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
left_complementable
right_complementable
complementable
)
Element
of the
carrier
of
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
=
r
: ( ( ) (
V33
()
real
ext-real
)
Real
)
(#)
(
seq_id
u
: ( ( ) (
left_complementable
right_complementable
complementable
)
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) ) ) ;
definition
func
l_scalar
->
( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
V40
()
V41
()
V42
() )
Function
of
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
means
:: RSSPACE:def 12
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) &
y
: ( ( ) ( )
set
)
in
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) holds
it
: ( ( ) ( )
set
)
.
(
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
Sum
(
(
seq_id
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
(#)
(
seq_id
y
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
)
: ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
:]
: ( ( ) (
V40
()
V41
()
V42
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ) ;
end;
registration
cluster
UNITSTR
(#
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
(
Zero_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( ( ) ( )
Element
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Add_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Mult_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
l_scalar
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
V40
()
V41
()
V42
() )
Function
of
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ) #) : ( (
strict
) ( non
empty
strict
)
UNITSTR
)
->
non
empty
strict
;
end;
definition
func
l2_Space
->
( ( non
empty
) ( non
empty
)
UNITSTR
)
equals
:: RSSPACE:def 13
UNITSTR
(#
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
(
Zero_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( ( ) ( )
Element
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Add_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
BinOp
of
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
(
Mult_
(
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
Linear_Space_of_RealSequences
: ( ( ) ( non
empty
left_complementable
right_complementable
complementable
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RLSStruct
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
-valued
Function-like
V14
(
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
)
Function
of
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ) ,
l_scalar
: ( (
Function-like
quasi_total
) (
Relation-like
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
V14
(
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) )
quasi_total
V40
()
V41
()
V42
() )
Function
of
[:
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of ) ,
the_set_of_l2RealSequences
: ( ( ) ( non
empty
linearly-closed
)
Subset
of )
:]
: ( ( ) ( )
set
) ,
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ) #) : ( (
strict
) ( non
empty
strict
)
UNITSTR
) ;
end;
theorem
:: RSSPACE:15
for
l
being ( ( ) ( )
RLSStruct
) st
RLSStruct
(# the
carrier
of
l
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) , the
ZeroF
of
l
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) ) , the
addF
of
l
: ( ( ) ( )
RLSStruct
) : ( (
Function-like
quasi_total
) (
Relation-like
[:
the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) , the
Mult
of
l
: ( ( ) ( )
RLSStruct
) : ( (
Function-like
quasi_total
) (
Relation-like
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
RLSStruct
) is ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) holds
l
: ( ( ) ( )
RLSStruct
) is ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
zeroed
)
RealLinearSpace
) ;
theorem
:: RSSPACE:16
for
rseq
being ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) holds
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) ) holds
(
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) is
summable
&
Sum
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RSSPACE:17
for
rseq
being ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) holds
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
<=
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) ) ) &
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) is
summable
&
Sum
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) holds
for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) holds
rseq
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
)
-valued
Function-like
non
empty
V14
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) )
quasi_total
V40
()
V41
()
V42
() )
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V33
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) )
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V33
()
real
ext-real
V38
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
()
V64
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V59
()
V60
()
V61
()
V62
()
V63
()
V64
()
V65
() )
Element
of
bool
REAL
: ( ( ) ( non
empty
V53
()
V59
()
V60
()
V61
()
V65
() )
set
) : ( ( ) ( )
set
) ) ) ;
registration
cluster
l2_Space
: ( ( non
empty
) ( non
empty
)
UNITSTR
)
->
non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
;
end;