:: GRSOLV_1 semantic presentation

begin

definition
let IT be ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ;
attr IT is solvable means :: GRSOLV_1:def 1
 ex F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) st
( len F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( Function-like functional empty V28() V29() V30() V32() V33() V34() V35() ext-real V107() FinSequence-membered ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (Omega). IT : ( ( ) ( ) doubleLoopStr ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( ) ( ) doubleLoopStr ) ) & F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . (len F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (1). IT : ( ( ) ( ) doubleLoopStr ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( ) ( ) doubleLoopStr ) ) & ( for i being ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
for G1, G2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( ) ( ) doubleLoopStr ) ) st G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . (i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) holds
( G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) is ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) & ( for N being ( ( normal ) ( non empty Group-like associative normal ) Subgroup of G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) st N : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) = G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) holds
G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ./. N : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of IT : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) is commutative ) ) ) );
end;

registration
cluster non empty strict Group-like associative solvable for ( ( ) ( ) multMagma ) ;
end;

theorem :: GRSOLV_1:1
for G being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for H, F1, F2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st F1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( normal ) ( non empty Group-like associative normal ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) holds
F1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) /\ H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( normal ) ( non empty Group-like associative normal ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) /\ H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ;

theorem :: GRSOLV_1:2
for G being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for F2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for F1 being ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) ) * F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: GRSOLV_1:3
for G being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for H, F2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for F1 being ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) )
for G2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) /\ F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
for G1 being ( ( normal ) ( non empty Group-like associative normal ) Subgroup of G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) st G1 : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b5 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) = H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) /\ F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
ex G3 being ( ( ) ( non empty Group-like associative ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ) st G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. G1 : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b5 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ,G3 : ( ( ) ( non empty Group-like associative ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. b4 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ) are_isomorphic ;

theorem :: GRSOLV_1:4
for G being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for H, F2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for F1 being ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) )
for G2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) /\ H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
for G1 being ( ( normal ) ( non empty Group-like associative normal ) Subgroup of G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) st G1 : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b5 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) = F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) /\ H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
ex G3 being ( ( ) ( non empty Group-like associative ) Subgroup of F2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. F1 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ) st G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. G1 : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b5 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ,G3 : ( ( ) ( non empty Group-like associative ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. b4 : ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of b3 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) ) are_isomorphic ;

theorem :: GRSOLV_1:5
for G being ( ( non empty strict Group-like associative solvable ) ( non empty strict Group-like associative solvable ) Group)
for H being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative solvable ) ( non empty strict Group-like associative solvable ) Group) ) holds H : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative solvable ) ( non empty strict Group-like associative solvable ) Group) ) is solvable ;

theorem :: GRSOLV_1:6
for G being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) st ex F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) st
( len F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( Function-like functional empty V28() V29() V30() V32() V33() V34() V35() ext-real V107() FinSequence-membered ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (Omega). G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( strict ) ( non empty strict Group-like associative normal ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) & F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . (len F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (1). G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( strict ) ( non empty V51() V52() 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element strict Group-like associative commutative normal cyclic ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) & ( for i being ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
for G1, G2 being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like ) FinSequence of Subgroups b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) . (i : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V28() V29() V30() V34() V35() ext-real V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) holds
( G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) & ( for N being ( ( normal ) ( non empty Group-like associative normal ) Subgroup of G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) st N : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) = G2 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
G1 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ./. N : ( ( normal ) ( non empty Group-like associative normal ) Subgroup of b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( non empty strict Group-like associative ) multMagma ) is ( ( non empty Group-like associative cyclic ) ( non empty Group-like associative commutative cyclic ) Group) ) ) ) ) holds
G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) is solvable ;

theorem :: GRSOLV_1:7
for G being ( ( non empty strict Group-like associative commutative ) ( non empty strict Group-like associative commutative ) Group) holds G : ( ( non empty strict Group-like associative commutative ) ( non empty strict Group-like associative commutative ) Group) is solvable ;

definition
let G, H be ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ;
let g be ( ( Function-like quasi_total V103(G : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ,H : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) ( Relation-like the carrier of G : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of H : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(G : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ,H : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ,H : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ;
let A be ( ( ) ( non empty Group-like associative ) Subgroup of G : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) ) ;
func g | A -> ( ( Function-like quasi_total V103(A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total unity-preserving V103(A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Homomorphism of A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: GRSOLV_1:def 2
g : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) | the carrier of A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like ) Element of K19(K20( the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let G, H be ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ;
let g be ( ( Function-like quasi_total V103(G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ;
let A be ( ( ) ( non empty Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ;
func g .: A -> ( ( strict ) ( non empty strict Group-like associative ) Subgroup of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: GRSOLV_1:def 3
 Image (g : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) | A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ) : ( ( Function-like quasi_total V103(A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total unity-preserving V103(A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Homomorphism of A : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of H : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: GRSOLV_1:8
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for g being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds the carrier of (g : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) = g : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: the carrier of A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: GRSOLV_1:9
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds Image (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) | A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( Function-like quasi_total V103(b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b4 : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( strict ) ( non empty strict Group-like associative ) Subgroup of Image h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ;

theorem :: GRSOLV_1:10
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( strict ) ( non empty strict Group-like associative ) Subgroup of Image h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ;

theorem :: GRSOLV_1:11
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) holds
( h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: ((1). G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty V51() V52() 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element strict Group-like associative commutative normal cyclic ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = (1). H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( strict ) ( non empty V51() V52() 1 : ( ( ) ( non empty V28() V29() V30() V34() V35() ext-real positive V107() ) Element of NAT : ( ( ) ( non empty V28() V29() V30() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element strict Group-like associative commutative normal cyclic ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) & h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: ((Omega). G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative normal ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) = (Omega). (Image h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative normal ) Subgroup of Image b3 : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ) ;

theorem :: GRSOLV_1:12
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A, B being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( ) ( non empty Group-like associative ) Subgroup of B : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) holds
h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( ) ( non empty Group-like associative ) Subgroup of h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: B : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ;

theorem :: GRSOLV_1:13
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) . a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) * (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) * (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) . a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: (A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: GRSOLV_1:14
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A, B being ( ( ) ( ) Subset of ) holds (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) * (h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: (A : ( ( ) ( ) Subset of ) * B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: GRSOLV_1:15
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) )
for A, B being ( ( strict ) ( non empty strict Group-like associative ) Subgroup of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of B : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) holds
h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: A : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is ( ( strict normal ) ( non empty strict Group-like associative normal ) Subgroup of h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) .: B : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ;

theorem :: GRSOLV_1:16
for G, H being ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group)
for h being ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,H : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) st G : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) is ( ( non empty Group-like associative solvable ) ( non empty Group-like associative solvable ) Group) holds
Image h : ( ( Function-like quasi_total V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total unity-preserving V103(b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of b1 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ,b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) : ( ( strict ) ( non empty strict Group-like associative ) Subgroup of b2 : ( ( non empty strict Group-like associative ) ( non empty strict Group-like associative ) Group) ) is solvable ;