:: PARSP_2 semantic presentation

begin

theorem :: PARSP_2:1
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) holds MPS 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) : ( ( ) ( non empty strict ) ParStr ) is ( ( non empty ParSp-like ) ( non empty ParSp-like ) ParSp) ;

theorem :: PARSP_2:2
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 :: PARSP_2:3
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 :: PARSP_2:4
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 :: PARSP_2:5
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 :: PARSP_2:6
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) holds
not for a, b, c being ( ( ) ( ) 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 :: PARSP_2:7
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 :: PARSP_2:8
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 :: PARSP_2:def 1
( 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;

registration
cluster non empty strict ParSp-like FanodesSp-like for ( ( ) ( ) ParStr ) ;
end;

definition
mode FanodesSp is ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) ParSp) ;
end;

theorem :: PARSP_2:9
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) 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 be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;
pred a,b,c is_collinear means :: PARSP_2:def 2
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 :: PARSP_2:10
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 :: PARSP_2:11
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 :: PARSP_2:12
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 ) ) or b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: PARSP_2:13
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 :: PARSP_2:14
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: PARSP_2:15
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 ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:16
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 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 ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: PARSP_2:17
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 :: PARSP_2:18
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for o, a, b, x being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear or not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear or not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear or o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: PARSP_2:19
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 :: PARSP_2:20
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 :: PARSP_2:21
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 ) ) & 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 ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:22
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 ) ) & 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 ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:23
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 ) ) ;

theorem :: PARSP_2:24
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 ) ) & 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 ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: PARSP_2:25
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 ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

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 :: PARSP_2:def 3
( 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 :: PARSP_2:26
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
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: PARSP_2:27
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 :: PARSP_2:28
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 :: PARSP_2:29
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 :: PARSP_2:30
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 ) ) ;

theorem :: PARSP_2:31
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 c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:32
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 b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:33
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 :: PARSP_2:34
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 not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
ex 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 ) ) ;

theorem :: PARSP_2:35
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 :: PARSP_2:36
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 ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:37
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 parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:38
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: PARSP_2:39
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 :: PARSP_2:40
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 :: PARSP_2:41
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 :: PARSP_2:42
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 ) ) ;

theorem :: PARSP_2:43
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex 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 ) ) ;

theorem :: PARSP_2:44
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex b, c 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 ) ) ;

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 :: PARSP_2:def 4
( ( 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 :: PARSP_2:45
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 ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:46
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 ) ) congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:47
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:48
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 ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:49
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 ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:50
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 :: PARSP_2:51
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
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:52
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 :: PARSP_2:53
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, b, c, x, y being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:54
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 ) ) ex 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 ) ) ;

theorem :: PARSP_2:55
for FdSp being ( ( non empty ParSp-like FanodesSp-like ) ( non empty ParSp-like FanodesSp-like ) FanodesSp)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:56
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 ) ) ;

theorem :: PARSP_2:57
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 ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: PARSP_2:58
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 ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) congr d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;