:: ANALOAF semantic presentation

begin

definition
let V be ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let u, v, w, y be ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;
pred u,v // w,y means :: ANALOAF:def 1
( u : ( ( ) ( ) M2(V : ( ( ) ( ) RLSStruct ) )) = v : ( ( V31() V37([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(V : ( ( ) ( ) RLSStruct ) ) V31() V37([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) or w : ( ( V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(V : ( ( ) ( ) RLSStruct ) ) V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) = y : ( ( ) ( ) M2(V : ( ( ) ( ) RLSStruct ) )) or ex a, b being ( ( ) ( V1() V14() V15() ) Real) st
( 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) < a : ( ( ) ( V1() V14() V15() ) Real) & 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) < b : ( ( ) ( V1() V14() V15() ) Real) & a : ( ( ) ( V1() V14() V15() ) Real) * (v : ( ( V31() V37([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(V : ( ( ) ( ) RLSStruct ) ) V31() V37([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) - u : ( ( ) ( ) M2(V : ( ( ) ( ) RLSStruct ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) )) = b : ( ( ) ( V1() V14() V15() ) Real) * (y : ( ( ) ( ) M2(V : ( ( ) ( ) RLSStruct ) )) - w : ( ( V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(V : ( ( ) ( ) RLSStruct ) ) V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) )) ) );
end;

theorem :: ANALOAF:1
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, v, u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds (w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ;

theorem :: ANALOAF:2
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for y, u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ;

theorem :: ANALOAF:3
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V1() V14() V15() ) Real) holds a : ( ( ) ( V1() V14() V15() ) Real) * (u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = - (a : ( ( ) ( V1() V14() V15() ) Real) * (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ;

theorem :: ANALOAF:4
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V1() V14() V15() ) Real) holds (a : ( ( ) ( V1() V14() V15() ) Real) - b : ( ( ) ( V1() V14() V15() ) Real) ) : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * (u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = (b : ( ( ) ( V1() V14() V15() ) Real) - a : ( ( ) ( V1() V14() V15() ) Real) ) : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ;

theorem :: ANALOAF:5
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V1() V14() V15() ) Real) st a : ( ( ) ( V1() V14() V15() ) Real) <> 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( V1() V14() V15() ) Real) ") : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ;

theorem :: ANALOAF:6
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V1() V14() V15() ) Real) holds
( ( a : ( ( ) ( V1() V14() V15() ) Real) <> 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) implies u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( V1() V14() V15() ) Real) ") : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ) & ( a : ( ( ) ( V1() V14() V15() ) Real) <> 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( V1() V14() V15() ) Real) ") : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) implies a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: ANALOAF:7
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
ex a, b being ( ( ) ( V1() V14() V15() ) Real) st
( a : ( ( ) ( V1() V14() V15() ) Real) * (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = b : ( ( ) ( V1() V14() V15() ) Real) * (y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) & 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) < a : ( ( ) ( V1() V14() V15() ) Real) & 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) < b : ( ( ) ( V1() V14() V15() ) Real) ) ;

theorem :: ANALOAF:8
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: ANALOAF:9
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:10
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: ANALOAF:11
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for p, q, u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: ANALOAF:12
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:13
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: ANALOAF:14
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( not u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) or u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) or u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:15
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, u, y, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: ANALOAF:16
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for y, v, w, u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:17
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex p, q being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ex y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:18
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for p, v, w, u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
ex y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:19
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st ( for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( V1() V14() V15() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( a : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & b : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) ) ) holds
( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ) ;

theorem :: ANALOAF:20
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( a : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & b : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) ) holds
ex u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
( not u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: ANALOAF:21
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex p, q being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
for w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ex a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * q : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
for u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st not u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & not u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
ex z being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
( ( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) or u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) & ( w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) or w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ) ;

definition
attr c1 is strict ;
struct AffinStruct -> ( ( ) ( ) 1-sorted ) ;
aggr AffinStruct(# carrier, CONGR #) -> ( ( strict ) ( strict ) AffinStruct ) ;
sel CONGR c1 -> ( ( ) ( V26() V29([: the carrier of c1 : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of c1 : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) ;
end;

registration
cluster non trivial strict for ( ( ) ( ) AffinStruct ) ;
end;

definition
let AS be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred a,b // c,d means :: ANALOAF:def 2
[[a : ( ( ) ( ) M2(AS : ( ( ) ( ) RLSStruct ) )) ,b : ( ( V31() V37([:AS : ( ( ) ( ) RLSStruct ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:AS : ( ( ) ( ) RLSStruct ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(AS : ( ( ) ( ) RLSStruct ) ) V31() V37([:AS : ( ( ) ( ) RLSStruct ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:AS : ( ( ) ( ) RLSStruct ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) ] : ( ( ) ( non empty ) M2([: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) )) ,[c : ( ( V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) ) ) ( V26() V29([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ) V30(AS : ( ( ) ( ) RLSStruct ) ) V31() V37([:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) ) ) M2( bool [:[:REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) ,AS : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )) ,d : ( ( ) ( ) M2(AS : ( ( ) ( ) RLSStruct ) )) ] : ( ( ) ( non empty ) M2([: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) )) ] : ( ( ) ( non empty ) M2([:[: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,[: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) )) in the CONGR of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( V26() V29([: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of AS : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) ;
end;

definition
let V be ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
func DirPar V -> ( ( ) ( V26() V29([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) means :: ANALOAF:def 3
 for x, z being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in it : ( ( ) ( ) M2(V : ( ( ) ( ) RLSStruct ) )) iff ex u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) set ) = [u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) M2([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) )) & z : ( ( ) ( ) set ) = [w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) M2([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) )) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: ANALOAF:22
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( [[u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) M2([: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) )) ,[w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) M2([: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) )) ] : ( ( ) ( non empty ) M2([:[: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,[: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) )) in DirPar V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V26() V29([: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V30([: the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) ) Relation of ) iff u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) // w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

definition
let V be ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
func OASpace V -> ( ( strict ) ( strict ) AffinStruct ) equals :: ANALOAF:def 4
 AffinStruct(# the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ,(DirPar V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( V26() V29([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) #) : ( ( strict ) ( strict ) AffinStruct ) ;
end;

registration
let V be ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
cluster OASpace V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

theorem :: ANALOAF:23
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) ) holds
( ex a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for a, b, c, d, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & ex a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: ANALOAF:24
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex p, q being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
for w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ex a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is OAffinSpace-like means :: ANALOAF:def 5
( ( for a, b, c, d, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & ex a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) );
end;

registration
cluster non empty non trivial strict OAffinSpace-like for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode OAffinSpace is ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) AffinStruct ) ;
end;

theorem :: ANALOAF:25
for AS being ( ( non empty ) ( non empty ) AffinStruct ) holds
( ( ex a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for a, b, c, d, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & ex a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) iff AS : ( ( non empty ) ( non empty ) AffinStruct ) is ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) ) ;

theorem :: ANALOAF:26
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( V1() V14() V15() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( a : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & b : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) ) holds
OASpace V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) ;

definition
let IT be ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) ;
attr IT is 2-dimensional means :: ANALOAF:def 6
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) & ( c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) );
end;

registration
cluster non empty non trivial strict OAffinSpace-like 2-dimensional for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode OAffinPlane is ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinSpace) ;
end;

theorem :: ANALOAF:27
for AS being ( ( non empty ) ( non empty ) AffinStruct ) holds
( ( ex a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for a, b, c, d, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & ex a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ) iff AS : ( ( non empty ) ( non empty ) AffinStruct ) is ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) ) ;

theorem :: ANALOAF:28
for V being ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) st ex u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st
( ( for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( V1() V14() V15() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) = 0. V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) holds
( a : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) & b : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2( bool REAL : ( ( ) ( V16() V17() V18() V22() ) set ) : ( ( ) ( non empty ) set ) )) )) ) ) & ( for w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ex a, b being ( ( ) ( V1() V14() V15() ) Real) st w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) + (b : ( ( ) ( V1() V14() V15() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) )) ) ) holds
OASpace V : ( ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) ;