:: ORTSP_1 semantic presentation

begin

definition
let F be ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ;
let IT be ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ;
attr IT is OrtSp-like means :: ORTSP_1:def 1
 for a, b, c, d, x being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 0. IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( V53(IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 0. IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( V53(IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 0. IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( V53(IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 0. IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( V53(IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) implies ex p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ) ) & ( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ implies b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ) & ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ implies ex k being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ) & ( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) _|_ & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) _|_ implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) _|_ ) );
end;

registration
let F be ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict OrtSp-like for ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ;
end;

definition
let F be ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ;
mode OrtSp of F is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ;
end;

theorem :: ORTSP_1:1
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:2
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:3
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:4
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:5
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) _|_ ) ;

theorem :: ORTSP_1:6
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:7
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b, d, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:8
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for k, l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
k : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:9
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:10
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) st (1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) + (1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) & ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 0. S : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( V53(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) holds
ex b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

definition
let F be ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ;
let S be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ;
let a, b, x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;
func ProJ (a,b,x) -> ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) means :: ORTSP_1:def 2
 for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) _|_ holds
it : ( ( ) ( V1() V4(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;
end;

theorem :: ORTSP_1:11
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;

theorem :: ORTSP_1:12
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:13
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) + (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:14
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = (l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) * (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:15
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) holds
ProJ ((l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:16
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, p, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
( ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: ORTSP_1:17
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, p, c 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 ) ) _|_ holds
ProJ ((a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:18
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:19
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:20
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ iff ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: ORTSP_1:21
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, q, p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
(ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * ((ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) = ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:22
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:23
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = - (ProJ (c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:24
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
ProJ (c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = ((ProJ (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) * (ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:25
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for p, a, x, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
(ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) = (ProJ (q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:26
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for p, a, x, q, b, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
((ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) * (ProJ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) = ((ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) * (ProJ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:27
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for a, p, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & not p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
(ProJ (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) = (ProJ (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

definition
let F be ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ;
let S be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ;
let x, y, a, b be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ;
func PProJ (a,b,x,y) -> ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) means :: ORTSP_1:def 3
 for q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) _|_ holds
it : ( ( ) ( ) Element of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) = ((ProJ (a : ( ( Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( V1() V4(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (ProJ (q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) * (ProJ (x : ( ( Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) if ex p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( not a : ( ( Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) _|_ & not x : ( ( Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) ( V1() V4([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Function-like V18([:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) ) Element of bool [:[:S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) SymStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) _|_ )
otherwise it : ( ( ) ( ) Element of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( V53(F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) ) ) Element of the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) ;
end;

theorem :: ORTSP_1:28
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. S : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( V53(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) holds
PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:29
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
( PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( V53(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ ) ;

theorem :: ORTSP_1:30
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:31
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = l : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) * (PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: ORTSP_1:32
for F being ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field)
for S being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) )
for b, a, x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) _|_ holds
PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like ) OrtSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = (PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) + (PProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V116() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V116() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) ;