:: EXTENS_1 semantic presentation

begin

begin

theorem :: EXTENS_1:1
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) c= X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EXTENS_1:2
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for M being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: M : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EXTENS_1:3
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for M1, M2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st M1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) c= M2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
(F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || M2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b6 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: M1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: M1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EXTENS_1:4
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B, C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds (G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b7 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** (F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b7 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b7 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EXTENS_1:5
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EXTENS_1:6
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" ;

begin

theorem :: EXTENS_1:7
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds doms (F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= doms F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EXTENS_1:8
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds rngs (F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= rngs F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EXTENS_1:9
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
( F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" iff rngs F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EXTENS_1:10
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for X being ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) holds rngs (Reverse X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of FreeGen b2 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of FreeMSA b2 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) ,b2 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) = X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EXTENS_1:11
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B, C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for X being ( ( V2() ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st rngs F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= X : ( ( V2() ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
(G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( V2() ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b7 : ( ( V2() ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V37() ) set ) = G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

begin

theorem :: EXTENS_1:12
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
( F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" iff for C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for G, H being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = H : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = H : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b5 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ;

theorem :: EXTENS_1:13
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is V2() holds
( F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" iff for C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for G, H being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V37() ) set ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** H : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V37() ) set ) holds
G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = H : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b5 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ;

begin

theorem :: EXTENS_1:14
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for X being ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )
for h1, h2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism FreeMSA X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism FreeMSA X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) || (FreeGen X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of FreeMSA b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of FreeGen b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of FreeMSA b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) || (FreeGen X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of FreeMSA b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of FreeGen b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of FreeMSA b3 : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ;

theorem :: EXTENS_1:15
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U1, U2 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for F being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_epimorphism U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) holds
for U3 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for h1, h2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ** F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of b5 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ** F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of b5 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ;

theorem :: EXTENS_1:16
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U2, U3 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for F being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) holds
( F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_monomorphism U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) iff for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for h1, h2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ** h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of the Sorts of b5 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ** h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of the Sorts of b5 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) ;

registration
let S be ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ;
let U1 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ;
cluster Relation-like V2() the carrier of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total for ( ( ) ( ) GeneratorSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) ;
end;

theorem :: EXTENS_1:17
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U1 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for A, B being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st A : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of B : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) holds
GenMSAlg A : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) is ( ( ) ( ) MSSubAlgebra of GenMSAlg B : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) ) ;

theorem :: EXTENS_1:18
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U1 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for U2 being ( ( ) ( ) MSSubAlgebra of U1 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) )
for B1 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for B2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st B1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) = B2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) holds
GenMSAlg B1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) = GenMSAlg B2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) ) ;

theorem :: EXTENS_1:19
for S being ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign )
for U1, U2 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) )
for Gen being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) )
for h1, h2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) is_homomorphism U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ,U2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) & h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) || Gen : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b4 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) || Gen : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b4 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
h1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) = h2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V37() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) ) ;