begin
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
(
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) iff ex
e,
f,
g,
h being ( ( ) ( )
Element of
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) st
(
[a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
Element of
[: the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) :] : ( ( ) ( )
set ) )
= [e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,h : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
set ) & ( ex
K being ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) ) st
(
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (h : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (h : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (h : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) ) or (
(e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
(e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
(e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) ) ) ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
a,
b,
c being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
for
e,
f,
g being ( ( ) ( )
Element of
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
[a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
Element of
[: the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) :] : ( ( ) ( )
set ) )
= [e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
set ) holds
(
e : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
<> f : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) &
e : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
<> g : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) &
f : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
<> g : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
a,
b,
c being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
for
e,
f,
g being ( ( ) ( )
Element of
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
for
K,
L being ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
[a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
Element of
[: the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) :] : ( ( ) ( )
set ) )
= [e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
set ) &
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= L : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= L : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= L : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
* ((e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) - (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) holds
(
K : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
L : ( ( ) ( )
Element of ( ( ) (
V4() non
trivial )
set ) )
= 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
for
e,
f,
g,
h being ( ( ) ( )
Element of
[: the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
[a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
Element of
[: the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) , the carrier of (MPS b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( non empty strict ) ParStr ) : ( ( ) ( V4() ) set ) :] : ( ( ) ( )
set ) )
= [e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ,h : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) ] : ( ( ) (
V1()
V2()
V3() )
set ) holds
(
h : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
`1_3 : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= ((f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) + (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `1_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
h : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
`2_3 : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= ((f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) + (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `2_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
h : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( )
set ) )
`3_3 : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
= ((f : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) + (g : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
- (e : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) , the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) : ( ( ) ( V4() non trivial ) set ) :] : ( ( ) ( ) set ) ) `3_3) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
b,
c,
a,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
(1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
+ (1_ F : ( ( non empty non degenerated right_complementable almost_left_invertible V91() V93() well-unital V99() Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed ) Field) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) )
<> 0. F : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V46(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) ) )
Element of the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field) : ( ( ) (
V4() non
trivial )
set ) ) &
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
F being ( ( non
empty non
degenerated right_complementable almost_left_invertible V91()
V93()
well-unital V99()
Abelian add-associative right_zeroed ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible unital V91()
V93()
right-distributive left-distributive right_unital well-unital V99()
left_unital Abelian add-associative right_zeroed )
Field)
for
a,
p,
b,
c,
q,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
definition
let IT be ( ( non
empty ParSp-like ) ( non
empty ParSp-like )
ParSp) ;
attr IT is
FanodesSp-like means
( not for
a,
b,
c being ( ( ) ( )
Element of ( ( ) ( )
set ) ) holds
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) & ( for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ) & ( for
a,
b,
c,
p,
q,
r being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ) );
end;
definition
let FdSp be ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp) ;
let a,
b,
c be ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
pred a,
b,
c is_collinear means
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'||' a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
c : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ;
end;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
(
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
p,
q,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
not
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
p,
q,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d,
x being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
x : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
x : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
o,
a,
b,
p,
q being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d,
p,
q being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
= q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
o,
a,
c,
b,
p,
q being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
o : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
= q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
definition
let FdSp be ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp) ;
let a,
b,
c,
d be ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
pred parallelogram a,
b,
c,
d means
( not
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
c : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) )
is_collinear &
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'||' c : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ,
d : ( (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) &
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
c : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) )
'||' b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
d : ( (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) );
end;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
( not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
( not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear & not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d,
x being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
( not
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) or not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
x : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear or not
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
x : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
(
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
p,
q being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
= q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
p,
b,
q,
c,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
b,
q,
c,
a,
p,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st not
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
parallelogram b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
p,
q,
r being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
<> c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
parallelogram b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
p,
b,
q,
c,
r,
d,
s being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
parallelogram b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
'||' r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
definition
let FdSp be ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp) ;
let a,
b,
r,
s be ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
pred a,
b congr r,
s means
( (
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) )
= b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) &
r : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) )
= s : ( (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) or ex
p,
q being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st
(
parallelogram p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ,
b : ( (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[:a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) &
parallelogram p : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
q : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
r : ( ( ) ( )
Element of
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ,
s : ( (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) ) (
V12()
V18(
[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) ,
a : ( ( ) ( )
VectSpStr over
FdSp : ( ( ) ( )
ParStr ) ) ) )
Element of
bool [:[: the carrier of FdSp : ( ( ) ( ) ParStr ) : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( ) set ) ,a : ( ( ) ( ) VectSpStr over FdSp : ( ( ) ( ) ParStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) );
end;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
congr c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) & not
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear holds
parallelogram a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
a,
b,
c,
d,
r,
s being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
congr c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
is_collinear &
parallelogram r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
parallelogram r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;
theorem
for
FdSp being ( ( non
empty ParSp-like FanodesSp-like ) ( non
empty ParSp-like FanodesSp-like )
FanodesSp)
for
r,
s,
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) st
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
congr a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) &
r : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
s : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
congr c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) holds
a : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) )
congr c : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4() )
set ) ) ;