:: POLYNOM6 semantic presentation

begin

notation
let L1, L2 be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
synonym L1,L2 are_isomorphic for L1 is_ringisomorph_to L2;
end;

definition
let L1, L2 be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
:: original: are_isomorphic
redefine pred L1 is_ringisomorph_to L2;
reflexivity
for L1 being ( ( non empty ) ( non empty ) doubleLoopStr ) holds R83(b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ,b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ;
end;

theorem :: POLYNOM6:1
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for B being ( ( ) ( ) set ) st ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) iff ex o being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) st
( x : ( ( ) ( ) set ) = o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) & o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) ) ) holds
o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) = o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

registration
let o1 be ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ;
let o2 be ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ;
cluster o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -> ordinal non empty ;
cluster o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) +^ o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -> ordinal non empty ;
end;

theorem :: POLYNOM6:2
for n being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for a, b being ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of n : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) st a : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) < b : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) holds
ex o being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) st
( o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in n : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) & a : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) . o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real ) set ) < b : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) . o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real ) set ) & ( for l being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) st l : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) holds
a : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) . l : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real ) set ) = b : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) . l : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real ) set ) ) ) ;

begin

definition
let o1, o2 be ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ;
let a be ( ( ) ( Relation-like o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;
let b be ( ( ) ( Relation-like o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;
func a +^ b -> ( ( ) ( Relation-like o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) means :: POLYNOM6:def 1
 for o being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) holds
( ( o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in o1 : ( ( non empty ) ( non empty ) set ) implies it : ( ( ) ( ) Element of o1 : ( ( non empty ) ( non empty ) set ) ) . o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( ) set ) = a : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( ) set ) ) & ( o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) \ o1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of K48((o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( ) set ) ) implies it : ( ( ) ( ) Element of o1 : ( ( non empty ) ( non empty ) set ) ) . o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( ) set ) = b : ( ( Function-like V28(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . (o : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -^ o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( ) set ) ) );
end;

theorem :: POLYNOM6:3
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for a being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) = {} : ( ( ) ( ) set ) holds
a : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = a : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYNOM6:4
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for a being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) = {} : ( ( ) ( ) set ) holds
a : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = b : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYNOM6:5
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds
( b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = EmptyBag (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) iff ( b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = EmptyBag o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = EmptyBag o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: POLYNOM6:6
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for c being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex c1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex c2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st c : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYNOM6:7
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b1, c1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2, c2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds
( b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYNOM6:8
for n being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for L being ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr )
for p, q, r being ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) holds (p : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) + q : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of K48(K49((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) *' r : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of K48(K49((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (p : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) *' r : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of K48(K49((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) + (q : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) *' r : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Series of ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of K48(K49((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of K48(K49((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative distributive ) ( non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

begin

registration
let n be ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ;
let L be ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ;
cluster Polynom-Ring (n : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ,L : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive right_unital well-unital left_unital ) doubleLoopStr ) -> non empty non trivial strict distributive ;
end;

definition
let o1, o2 be ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ;
let L be ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ;
let P be ( ( Function-like V28( Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) )) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) V250( Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) ) ) ( Relation-like Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) )) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V28( Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) )) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) V250( Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) ) ) Polynomial of ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty right_complementable strict add-associative right_zeroed ) doubleLoopStr ) ) ;
func Compress P -> ( ( Function-like V28( Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V250( Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like V28( Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V250( Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Polynomial of ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) means :: POLYNOM6:def 2
 for b being ( ( ) ( Relation-like o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex b1 being ( ( ) ( Relation-like o1 : ( ( non empty ) ( non empty ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex b2 being ( ( ) ( Relation-like o2 : ( ( non empty ) ( non empty ) ZeroStr ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex Q1 being ( ( Function-like V28( Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V250( Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like V28( Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V250( Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Polynomial of ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st
( Q1 : ( ( Function-like V28( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) V250( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) ( Relation-like Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) -valued Function-like V28( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) V250( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) Polynomial of ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) = P : ( ( Function-like V28(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(REAL : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . b1 : ( ( ) ( Relation-like o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (Polynom-Ring (o2 : ( ( non empty ) ( non empty ) ZeroStr ) ,L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) & b : ( ( ) ( Relation-like o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = b1 : ( ( ) ( Relation-like o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( non empty ) ( non empty ) set ) +^ o2 : ( ( non empty ) ( non empty ) ZeroStr ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & it : ( ( ) ( ) Element of o1 : ( ( non empty ) ( non empty ) set ) ) . b : ( ( ) ( Relation-like o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = Q1 : ( ( Function-like V28( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) V250( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) ( Relation-like Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) -valued Function-like V28( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) , the carrier of L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) V250( Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) Polynomial of ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ,L : ( ( non trivial right_complementable add-associative right_zeroed well-unital distributive ) ( non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) . b2 : ( ( ) ( Relation-like o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined o1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V28(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) ) Element of K48(K49(K49(o1 : ( ( non empty ) ( non empty ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,o1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: POLYNOM6:9
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b1, c1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2, c2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) divides c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) divides c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds
b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) divides c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYNOM6:10
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b being ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) )
for b1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st b : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) divides b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex c1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex c2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) divides b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) divides b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined Function-like total natural-valued finite-support ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) bag of b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) = c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYNOM6:11
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for a1, b1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for a2, b2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds
( a1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ a2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) < b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) iff ( a1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) < b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) or ( a1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & a2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) < b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ) ;

theorem :: POLYNOM6:12
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (Bags (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) st dom G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) = dom (divisors b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) & ( for i being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) st i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) in dom (divisors b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) holds
ex a19 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex Fk being ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) /. i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) Element of (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) & (divisors b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) /. i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = a19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & len Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len (divisors b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ( for m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) st m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) in dom Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) holds
ex a199 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( (divisors b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) /. m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = a199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) & Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) /. m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = a19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ a199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ) ) holds
divisors (b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) FinSequence of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = FlattenSeq G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support ) Element of (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYNOM6:13
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for a1, b1, c1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for a2, b2, c2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -' a1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) set ) & c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) = b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -' a2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined Function-like total ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) set ) holds
(b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -' (a1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ a2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) set ) = c1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ c2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYNOM6:14
for o1, o2 being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal)
for b1 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for b2 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) st dom G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) = dom (decomp b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) & ( for i being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) st i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) in dom (decomp b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) holds
ex a19, b19 being ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ex Fk being ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (o1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) st
( Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) = G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) /. i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) Element of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & (decomp b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) /. i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) = <*a19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ,b19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like non empty Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) & len Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len (decomp b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ( for m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) st m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) in dom Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Element of K48(NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non trivial non finite ) set ) ) holds
ex a199, b199 being ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags o2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( (decomp b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) /. m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) = <*a199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ,b199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like non empty Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) & Fk : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) /. m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) = <*(a19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ a199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ,(b19 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b199 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like non empty Function-yielding V36() finite 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like FinSubsequence-like finite-support ) Element of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ) ) ) holds
decomp (b1 : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) +^ b2 : ( ( ) ( Relation-like b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( functional non empty ) Element of K48((Bags b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) -defined RAT : ( ( ) ( ) set ) -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support ) Element of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) = FlattenSeq G : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) FinSequence of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support ) Element of (2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of 2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive ) Element of NAT : ( ( ) ( epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal ) Element of K48(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -tuples_on (Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( functional non empty ) Element of K48((Bags (b1 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) +^ b2 : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: POLYNOM6:15
for o1, o2 being ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal)
for L being ( ( non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) holds Polynom-Ring (o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,(Polynom-Ring (o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ,L : ( ( non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) )) : ( ( non empty strict ) ( non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) , Polynom-Ring ((o1 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) +^ o2 : ( ( ordinal non empty ) ( epsilon-transitive epsilon-connected ordinal non empty ) Ordinal) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal non empty ) set ) ,L : ( ( non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( non empty strict ) ( non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) are_isomorphic ;