:: RLVECT_X semantic presentation
begin
theorem
:: RLVECT_X:1
for
X
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
R1
,
R2
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) st
len
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) holds
Sum
(
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
+
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
Sum
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
Sum
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RLVECT_X:2
for
X
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
R1
,
R2
,
R3
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) st
len
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) &
R3
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
=
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
-
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) , the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
Sum
R3
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
Sum
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
-
(
Sum
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RLVECT_X:3
for
X
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
R1
,
R2
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
a
being ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) st
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
(#)
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) , the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
Sum
R2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
Sum
R1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ;
begin
definition
let
V
be ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ;
let
i
be ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) ;
let
L
be ( ( ) (
Relation-like
the
carrier
of
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) ;
func
i
*
L
->
( ( ) (
Relation-like
the
carrier
of
V
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
V
: ( ( ) ( )
RLSStruct
) )
means
:: RLVECT_X:def 1
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( )
set
) ) holds
it
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
)
-defined
V
: ( ( ) ( )
RLSStruct
)
-valued
Function-like
quasi_total
)
Element
of
K19
(
K20
(
K20
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
=
i
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
RLSStruct
) )
*
(
L
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
V
: ( ( ) ( )
RLSStruct
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
)
-defined
V
: ( ( ) ( )
RLSStruct
)
-valued
Function-like
quasi_total
)
Element
of
K19
(
K20
(
K20
(
V
: ( ( ) ( )
RLSStruct
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
) ,
V
: ( ( ) ( )
RLSStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
ext-real
V31
()
V32
() )
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) ;
end;
definition
let
V
be ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
Z_Lin
A
->
( ( ) ( )
Subset
of )
equals
:: RLVECT_X:def 2
{
(
Sum
l
: ( ( ) (
Relation-like
the
carrier
of
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Subset
of ) )
)
: ( ( ) ( )
Element
of the
carrier
of
V
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
) ) where
l
is ( ( ) (
Relation-like
the
carrier
of
V
: ( ( ) ( )
RLSStruct
) : ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
RLSStruct
) ) ) :
rng
l
: ( ( ) (
Relation-like
the
carrier
of
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
}
;
end;
theorem
:: RLVECT_X:4
for
a
being ( ( ) (
ext-real
V31
()
V32
() )
Real
)
for
i
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
l
being ( ( ) (
Relation-like
the
carrier
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Subset
of ) ) st
a
: ( ( ) (
ext-real
V31
()
V32
() )
Real
)
=
i
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) holds
a
: ( ( ) (
ext-real
V31
()
V32
() )
Real
)
*
l
: ( ( ) (
Relation-like
the
carrier
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
4
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
Relation-like
the
carrier
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) )
=
i
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
l
: ( ( ) (
Relation-like
the
carrier
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
4
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
Relation-like
the
carrier
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
3
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) ;
theorem
:: RLVECT_X:5
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
l1
,
l2
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Subset
of ) ) st
rng
l1
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
2
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) &
rng
l2
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
2
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) holds
rng
(
l1
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
2
: ( ( ) ( )
Subset
of ) )
+
l2
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
2
: ( ( ) ( )
Subset
of ) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ;
theorem
:: RLVECT_X:6
for
i
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
l
being ( ( ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
A
: ( ( ) ( )
Subset
of ) ) st
rng
l
: ( ( ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
3
: ( ( ) ( )
Subset
of ) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) holds
rng
(
i
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
l
: ( ( ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
3
: ( ( ) ( )
Subset
of ) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ;
theorem
:: RLVECT_X:7
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) holds
rng
(
ZeroLC
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
quasi_total
complex-valued
ext-real-valued
real-valued
)
Linear_Combination
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) : ( ( ) (
V117
()
V118
()
V119
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
c=
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ;
theorem
:: RLVECT_X:8
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
the
carrier
of
(
Lin
A
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) ( non
empty
V71
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
Subspace
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: RLVECT_X:9
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
,
u
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( )
Subset
of ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:10
for
i
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( )
Subset
of ) st
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
i
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:11
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
0.
V
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) (
V52
(
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:12
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
x
: ( ( ) ( )
set
)
in
A
: ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
set
)
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:13
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Z_Lin
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:14
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Z_Lin
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
Z_Lin
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
(
Z_Lin
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: RLVECT_X:15
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Z_Lin
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
c=
(
Z_Lin
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
Z_Lin
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: RLVECT_X:16
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
Z_Lin
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
V12
()
finite
1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) iff ex
a
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:17
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
{
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
V12
()
finite
1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:18
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
,
w
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
Z_Lin
{
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
V12
()
finite
1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) iff ex
a
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:19
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
w1
,
w2
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) iff ex
a
,
b
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
(
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:20
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
w1
,
w2
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:21
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
,
w1
,
w2
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) iff ex
a
,
b
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:22
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v1
,
v2
,
v3
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
Z_Lin
{
v1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
v2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
v3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) iff ex
a
,
b
,
c
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
(
(
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
v1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
v2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
c
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
v3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:23
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
w1
,
w2
,
w3
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) &
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) &
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: RLVECT_X:24
for
x
being ( ( ) ( )
set
)
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
v
,
w1
,
w2
,
w3
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
)
in
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
Z_Lin
{
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) ,
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) iff ex
a
,
b
,
c
being ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
(
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
+
(
a
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w1
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w2
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
c
: ( (
integer
) (
ext-real
V31
()
V32
()
integer
)
Integer
)
*
w3
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RLVECT_X:25
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) iff ex
g1
,
h1
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) ex
a1
being ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) st
(
x
: ( ( ) ( )
set
)
=
Sum
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) &
rng
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of ) &
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) &
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
a1
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) & ( for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
4
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
a1
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
)
.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
registration
let
D
be ( ( non
empty
) ( non
empty
)
set
) ;
let
n
be ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) ;
cluster
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
D
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
finite
n
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
)
-element
FinSequence-like
FinSubsequence-like
for ( ( ) ( )
set
) ;
end;
definition
let
RS
be ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ;
let
f
be ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) ;
func
Z_Lin
f
->
( ( ) ( )
Subset
of )
equals
:: RLVECT_X:def 3
{
(
Sum
g
: ( (
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
RS
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) where
g
is ( (
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-valued
Function-like
finite
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( )
set
) ) : ex
a
being ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) st
for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
)
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
g
: ( (
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
RS
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) )
=
(
a
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
)
.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
f
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
set
)
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) ( )
Element
of the
carrier
of
RS
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
RS
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) )
}
;
end;
theorem
:: RLVECT_X:26
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) iff ex
g
being ( (
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) ex
a
being ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) st
(
x
: ( ( ) ( )
set
)
=
Sum
g
: ( (
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) & ( for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
g
: ( (
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
a
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
)
.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
theorem
:: RLVECT_X:27
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
a
,
b
being ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) holds
(
a
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
b
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:28
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) st
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
=
(
Seg
(
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
)
: ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) )
-->
(
0.
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
)
: ( ( ) (
V52
(
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
quasi_total
) (
Relation-like
Seg
(
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
finite
FinSequence-like
FinSubsequence-like
)
Element
of
K19
(
K20
(
(
Seg
(
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
)
: ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) , the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
Sum
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
0.
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) (
V52
(
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RLVECT_X:29
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
v
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) &
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
=
(
(
Seg
(
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
)
: ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) )
-->
(
0.
RS
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
)
: ( ( ) (
V52
(
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
Seg
(
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
finite
FinSequence-like
FinSubsequence-like
)
Element
of
K19
(
K20
(
(
Seg
(
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
)
: ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) , the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
+*
(
{
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
}
: ( ( ) ( non
empty
V12
()
finite
V37
() 1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
set
)
-->
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
{
b
4
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
}
: ( ( ) ( non
empty
V12
()
finite
V37
() 1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
finite
)
Element
of
K19
(
K20
(
{
b
4
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
}
: ( ( ) ( non
empty
V12
()
finite
V37
() 1 : ( ( ) ( non
empty
ext-real
positive
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
set
) , the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
finite
)
set
) holds
Sum
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
v
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RLVECT_X:30
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
2
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:31
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) holds
rng
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
Z_Lin
f
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:32
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
g
,
h
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
s
being ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) st
rng
g
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
Z_Lin
f
: ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) &
len
g
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
s
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) &
len
g
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
h
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) & ( for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
g
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
3
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
h
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
s
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
)
.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
g
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) holds
Sum
h
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
Z_Lin
f
: ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:33
for
RS
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
f
being ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) holds
Z_Lin
(
rng
f
: ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
Z_Lin
f
: ( ( non
empty
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:34
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Lin
(
Z_Lin
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( (
strict
) ( non
empty
V71
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
Subspace
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) )
=
Lin
A
: ( ( ) ( )
Subset
of ) : ( (
strict
) ( non
empty
V71
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
Subspace
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) ;
theorem
:: RLVECT_X:35
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
set
)
for
g1
,
h1
being ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
a1
being ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) st
x
: ( ( ) ( )
set
)
=
Sum
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) &
rng
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
finite
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) &
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
=
len
a1
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) & ( for
i
being ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) st
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
in
Seg
(
len
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
finite
len
b
4
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Element
of
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) )
-element
)
Element
of
K19
(
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) ) ) : ( ( ) (
V12
() non
finite
)
set
) ) holds
h1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
=
(
a1
: ( (
Relation-like
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
FinSequence-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
INT
: ( ( ) ( non
empty
V12
() non
finite
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
complex-valued
ext-real-valued
real-valued
)
FinSequence
)
.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) (
ext-real
V31
()
V32
()
integer
)
Element
of
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) )
*
(
g1
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
V12
()
V24
()
V25
()
V26
() non
finite
cardinal
limit_cardinal
)
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V12
() non
finite
)
set
) ) : ( ( ) (
V12
() non
finite
)
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
i
: ( (
V30
() ) (
ext-real
V24
()
V25
()
V26
()
V30
()
V31
()
V32
()
finite
cardinal
integer
)
Nat
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) ) holds
x
: ( ( ) ( )
set
)
in
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:36
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Z_Lin
(
Z_Lin
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: RLVECT_X:37
for
V
being ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
Z_Lin
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
Z_Lin
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
Lin
A
: ( ( ) ( )
Subset
of ) : ( (
strict
) ( non
empty
V71
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
Subspace
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) )
=
Lin
B
: ( ( ) ( )
Subset
of ) : ( (
strict
) ( non
empty
V71
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
Subspace
of
b
1
: ( ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V71
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
)
RealLinearSpace
) ) ;