for X being ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace)
for Y being ( ( ) ( ) Subset of )
for L being ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) holds
( Y : ( ( ) ( ) Subset of ) is_summable_set_by L : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) iff for e being ( ( ) ( V36() real ext-real ) Real) st 0 : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real finite V47() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( ) set ) ) ) < e : ( ( ) ( V36() real ext-real ) Real) holds
ex Y0 being ( ( finite ) ( finite ) Subset of ) st
( not Y0 : ( ( finite ) ( finite ) Subset of ) is empty & Y0 : ( ( finite ) ( finite ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & ( for Y1 being ( ( finite ) ( finite ) Subset of ) st not Y1 : ( ( finite ) ( finite ) Subset of ) is empty & Y1 : ( ( finite ) ( finite ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & Y0 : ( ( finite ) ( finite ) Subset of ) misses Y1 : ( ( finite ) ( finite ) Subset of ) holds
abs (setopfunc (Y1 : ( ( finite ) ( finite ) Subset of ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) ,L : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) ,addreal : ( ( Function-like V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like V14([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ) V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) commutative associative having_a_unity ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) < e : ( ( ) ( V36() real ext-real ) Real) ) ) ) ;

for X being ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) st the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is commutative & the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is associative & the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is having_a_unity holds
for S being ( ( finite ) ( finite ) OrthogonalFamily of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) st not S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) is empty holds
for I being ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) st S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) c= dom I : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) & ( for y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st y : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) in S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) holds
I : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) . y : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = y : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
for H being ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) st S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) c= dom H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ) set ) & ( for y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) holds
H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) . y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) = y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
(setopfunc (S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,I : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) , the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) .|. (setopfunc (S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,I : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) , the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) = setopfunc (S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) ,H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Function of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ,addreal : ( ( Function-like V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like V14([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ) V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) commutative associative having_a_unity ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ;

for X being ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) st the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is commutative & the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is associative & the addF of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V14([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is having_a_unity holds
for S being ( ( finite ) ( finite ) OrthogonalFamily of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) st not S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) is empty holds
for H being ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) st S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) c= dom H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) holds
H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
(setsum S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) .|. (setsum S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) = setopfunc (S : ( ( finite ) ( finite ) OrthogonalFamily of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) ) , the carrier of X : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) ,H : ( ( Function-like V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty V14( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b₁ : ( ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) ( non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) Functional of ( ( ) ( non empty ) set ) ) ,addreal : ( ( Function-like V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like V14([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ) V18([:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) commutative associative having_a_unity ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V36() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite ) set ) ) ;