begin
theorem
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
u,
v,
w being ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
for
l being ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) ) st
u : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> v : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) &
u : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> w : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) &
v : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> w : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
Sum l : ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
= (((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) ) . u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) + ((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
+ ((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-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 ) ) ) . w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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
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 ) )
for
a,
b,
c being ( ( ) (
V24()
V25()
V41() )
Real) st
v1 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) &
v1 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> v3 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) &
v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
<> v3 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
ex
l being ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) ) st
(
l : ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) )
. v1 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V41() )
Element of
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
= a : ( ( ) (
V24()
V25()
V41() )
Real) &
l : ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) )
. v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V41() )
Element of
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
= b : ( ( ) (
V24()
V25()
V41() )
Real) &
l : ( ( ) (
V7()
V10( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) )
V11(
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
Function-like quasi_total )
Linear_Combination of
{b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) (
V26() )
Element of
K32( the
carrier of
b1 : ( ( non
empty V71()
Abelian add-associative right_zeroed vector-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 ) ) )
. v3 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V24()
V25()
V41() )
Element of
REAL : ( ( ) ( non
empty V5()
V26() )
set ) )
= c : ( ( ) (
V24()
V25()
V41() )
Real) ) ;