begin
registration
let F be ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) ;
let X be ( ( non
empty ) ( non
empty )
set ) ;
let md be ( (
V6()
V18(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) ) (
V1()
V4(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
V6()
V18(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let o be ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let mF be ( (
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) ) (
V1()
V4(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let mo be ( ( ) (
V1()
V4(
X : ( ( non
empty ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) ) )
Relation of ) ;
cluster SymStr(#
X : ( ( non
empty ) ( non
empty )
set ) ,
md : ( (
V6()
V18(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) ) (
V1()
V4(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
V6()
V18(
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) )
Element of
bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
o : ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
mF : ( (
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) ) (
V1()
V4(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) )
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
mo : ( ( ) (
V1()
V4(
X : ( ( non
empty ) ( non
empty )
set ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) ) )
Element of
bool [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
SymStr over
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) )
-> non
empty strict ;
end;
definition
let F be ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) ;
let S be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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
for
l being ( ( ) ( )
Element of ( ( ) ( non
empty non
trivial )
set ) ) st
a : ( (
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) )
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) )
Element of
bool [:[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
_|_ holds
it : ( ( ) (
V1()
V4(
S : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) ) )
Element of
bool [:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= l : ( ( ) ( )
Element of ( ( ) ( non
empty non
trivial )
set ) ) ;
end;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) )
for
a,
p,
q,
b being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) (
V51(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) & not
p : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
_|_ & not
q : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
_|_ & not
q : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
_|_ holds
(ProJ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of ( ( ) ( non
empty non
trivial )
set ) )
* (ProJ (b : ( ( ) ( ) 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) )
= (ProJ (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of ( ( ) ( non
empty non
trivial )
set ) )
* (ProJ (q : ( ( ) ( ) 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) )
for
p,
a,
x,
q being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) (
V51(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) & 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( 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 ) )
* (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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) )
for
p,
a,
x,
q,
b,
y being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) (
V51(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) & 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) ;
let S be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) ) ;
let x,
y,
a,
b be ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ;
assume
( not
a : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
_|_ &
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) Field) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) (
V51(
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) ) )
Element of the
carrier of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) )
;
func PProJ (
a,
b,
x,
y)
-> ( ( ) ( )
Element of ( ( ) ( non
empty non
trivial )
set ) )
means
for
q being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st not
a : ( (
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) ) (
V1()
V4(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) )
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) )
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
_|_ & not
x : ( (
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) )
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) )
Element of
bool [:[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) )
= ((ProJ (a : ( ( V6() V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) set ) ) V6() V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) 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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( V1() V4(S : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) set ) ) ) Element of bool [:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) 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 : ( ( V6() V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) set ) ) V6() V18([: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) 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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( V6() V18([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) ( V1() V4([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) set ) ) V6() V18([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) Element of bool [:[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
* (ProJ (x : ( ( V6() V18([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) ( V1() V4([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(S : ( ( ) ( ) set ) ) V6() V18([:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) ) Element of bool [:[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of S : ( ( ) ( ) 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
if ex
p being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st
( not
a : ( (
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) ) (
V1()
V4(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) )
V6()
V18(
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) )
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
_|_ & not
x : ( (
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
V5(
S : ( ( ) ( )
set ) )
V6()
V18(
[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) ) )
Element of
bool [:[:S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( )
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) : ( ( ) (
V51(
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) ) ;
end;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field)
for
S being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
F : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) )
for
b,
a,
x,
y,
z being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() 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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) (
V51(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) & 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 SymSp-like ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like )
SymSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
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 V114() ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114()
left_unital )
Field) : ( ( ) ( non
empty non
trivial )
set ) ) ;