:: ANALORT semantic presentation

begin

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y, u be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func Ortm (x,y,u) -> ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) equals :: ANALORT:def 1
((pr1 (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) * x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) + ((- (pr2 (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) ) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) * y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ;
end;

theorem :: ANALORT:1
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:2
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for n being ( ( ) ( V17() V27() V28() ) Real) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(n : ( ( ) ( V17() V27() V28() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = n : ( ( ) ( V17() V27() V28() ) Real) * (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:3
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(0. V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( V60(b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = 0. V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V60(b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:4
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(- u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = - (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:5
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - (Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:6
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:7
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:8
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y, u be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func Orte (x,y,u) -> ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) equals :: ANALORT:def 2
((pr2 (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) * x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) + ((- (pr1 (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) ) : ( ( ) ( V17() V27() V28() ) M2( REAL : ( ( ) ( V29() V30() V31() V35() ) set ) )) * y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ;
end;

theorem :: ANALORT:9
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(- v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = - (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:10
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:11
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:12
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for n being ( ( ) ( V17() V27() V28() ) Real) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(n : ( ( ) ( V17() V27() V28() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = n : ( ( ) ( V17() V27() V28() ) Real) * (Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:13
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:14
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,(Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = - u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ;

theorem :: ANALORT:15
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y, u, v, u1, v1 be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
pred u,v,u1,v1 are_COrte_wrt x,y means :: ANALORT:def 3
 Orte (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) , Orte (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,v : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) // u1 : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ,v1 : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ;
pred u,v,u1,v1 are_COrtm_wrt x,y means :: ANALORT:def 4
 Ortm (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,u : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) , Ortm (x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,v : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) // u1 : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ,v1 : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ;
end;

theorem :: ANALORT:16
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:17
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:18
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:19
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:20
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:21
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:22
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:23
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:24
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_Ort_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:25
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Orte (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:26
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) , Ortm (x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:27
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) iff ex u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ;

theorem :: ANALORT:28
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) // u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) iff ex u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ;

theorem :: ANALORT:29
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_Ort_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) iff ( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ;

theorem :: ANALORT:30
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:31
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:32
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:33
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:34
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, u1, v1, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:35
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, u1, v1, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:36
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:37
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, v, u1, v1, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:38
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ex u1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:39
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ex u1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:40
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ex u1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:41
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ex u1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) <> u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:42
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:43
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:44
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:45
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:46
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:47
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y, u, u1, v, v1, w, w1, u2, v2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;

theorem :: ANALORT:48
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for v, w, u1, v1, w1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex u2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( ( v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) & ( u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ;

theorem :: ANALORT:49
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & ( for v1, w1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or ( not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) or v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ) ;

theorem :: ANALORT:50
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
for v, w, u1, v1, w1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex u2 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( ( v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) & ( u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ;

theorem :: ANALORT:51
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
ex u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
( u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & ( for v1, w1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) or ( not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) or v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = w1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ) ) ;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func CORTE (V,x,y) -> ( ( ) ( V7() V10([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) means :: ANALORT:def 5
 for uu, vv being ( ( ) ( ) set ) holds
( [uu : ( ( ) ( ) set ) ,vv : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in it : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) iff ex u1, u2, v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st
( uu : ( ( ) ( ) set ) = [u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ] : ( ( ) ( ) set ) & vv : ( ( ) ( ) set ) = [v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ] : ( ( ) ( ) set ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) );
end;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func CORTM (V,x,y) -> ( ( ) ( V7() V10([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) means :: ANALORT:def 6
 for uu, vv being ( ( ) ( ) set ) holds
( [uu : ( ( ) ( ) set ) ,vv : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in it : ( ( V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) ( V7() V10([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11(V : ( ( ) ( ) ParOrtStr ) ) V12() V37([:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) ) ) M2( bool [:[:REAL : ( ( ) ( V29() V30() V31() V35() ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) iff ex u1, u2, v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st
( uu : ( ( ) ( ) set ) = [u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ] : ( ( ) ( ) set ) & vv : ( ( ) ( ) set ) = [v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ] : ( ( ) ( ) set ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) );
end;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func CESpace (V,x,y) -> ( ( strict ) ( strict ) AffinStruct ) equals :: ANALORT:def 7
 AffinStruct(# the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) ,(CORTE (V : ( ( ) ( ) ParOrtStr ) ,x : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ,y : ( ( ) ( V7() V10([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) V11([:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ) ) M2( bool [:[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) ,[:V : ( ( ) ( ) ParOrtStr ) ,V : ( ( ) ( ) ParOrtStr ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V7() V10([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) #) : ( ( strict ) ( strict ) AffinStruct ) ;
end;

registration
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
cluster CESpace (V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ,x : ( ( ) ( ) M2( the carrier of V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( V4() ) set ) )) ,y : ( ( ) ( ) M2( the carrier of V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( V4() ) set ) )) ) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

definition
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
func CMSpace (V,x,y) -> ( ( strict ) ( strict ) AffinStruct ) equals :: ANALORT:def 8
 AffinStruct(# the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) ,(CORTM (V : ( ( V46() ) ( V46() ) set ) ,x : ( ( ) ( ) set ) ,y : ( ( ) ( ) M2( the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V7() V10([: the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( V46() ) ( V46() ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) #) : ( ( strict ) ( strict ) AffinStruct ) ;
end;

registration
let V be ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let x, y be ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ;
cluster CMSpace (V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ,x : ( ( ) ( ) M2( the carrier of V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( V4() ) set ) )) ,y : ( ( ) ( ) M2( the carrier of V : ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( V4() ) set ) )) ) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

theorem :: ANALORT:52
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for uu being ( ( ) ( ) set ) holds
( uu : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) iff uu : ( ( ) ( ) set ) is ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:53
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for uu being ( ( ) ( ) set ) holds
( uu : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) iff uu : ( ( ) ( ) set ) is ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:54
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, u1, v1, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for p, q, r, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) iff u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrte_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: ANALORT:55
for V being ( ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, u1, v1, x, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for p, q, r, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) iff u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) are_COrtm_wrt x : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;