:: GRSOLV_1 semantic presentation begin definitionlet "IT" be ($#l3_algstr_0 :::"Group":::); attr "IT" is :::"solvable"::: means :: GRSOLV_1:def 1 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_group_3 :::"Subgroups"::: ) "IT") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) "IT")) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) "IT")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "IT" "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" ($#v5_group_1 :::"commutative"::: ) ) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"solvable"::: GRSOLV_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_grsolv_1 :::"solvable"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "IT"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "IT")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" ($#v5_group_1 :::"commutative"::: ) ) ")" ) ")" )) ")" ) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_grsolv_1 :::"solvable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GRSOLV_1:1 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "F1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H"))) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Set (Var "F2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H")))))) ; theorem :: GRSOLV_1:2 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "F1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "F2")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F2")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "F1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "F1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "F1")))))))) ; theorem :: GRSOLV_1:3 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "F1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "F2")) (Bool "for" (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G2")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H")) ($#k10_group_2 :::"/\"::: ) (Set (Var "F2"))))) "holds" (Bool "for" (Set (Var "G1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k10_group_2 :::"/\"::: ) (Set (Var "F1"))))) "holds" (Bool "ex" (Set (Var "G3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "F2")) ($#k5_group_6 :::"./."::: ) (Set (Var "F1"))) "st" (Bool (Set (Set (Var "G2")) ($#k5_group_6 :::"./."::: ) (Set (Var "G1"))) "," (Set (Var "G3")) ($#r1_group_6 :::"are_isomorphic"::: ) ))))))) ; theorem :: GRSOLV_1:4 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "F2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "F1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "F2")) (Bool "for" (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G2")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "F2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H"))))) "holds" (Bool "for" (Set (Var "G1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H"))))) "holds" (Bool "ex" (Set (Var "G3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "F2")) ($#k5_group_6 :::"./."::: ) (Set (Var "F1"))) "st" (Bool (Set (Set (Var "G2")) ($#k5_group_6 :::"./."::: ) (Set (Var "G1"))) "," (Set (Var "G3")) ($#r1_group_6 :::"are_isomorphic"::: ) ))))))) ; theorem :: GRSOLV_1:5 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_grsolv_1 :::"solvable"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "H")) "is" ($#v1_grsolv_1 :::"solvable"::: ) ))) ; theorem :: GRSOLV_1:6 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::)) ")" ) ")" )) ")" ) ")" ))) "holds" (Bool (Set (Var "G")) "is" ($#v1_grsolv_1 :::"solvable"::: ) )) ; theorem :: GRSOLV_1:7 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Var "G")) "is" ($#v1_grsolv_1 :::"solvable"::: ) )) ; definitionlet "G", "H" be ($#l3_algstr_0 :::"Group":::); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); let "A" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "g" :::"|"::: "A" -> ($#m1_subset_1 :::"Homomorphism":::) "of" "A" "," "H" equals :: GRSOLV_1:def 2 (Set "g" ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); end; :: deftheorem defines :::"|"::: GRSOLV_1:def 2 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "g")) ($#k1_grsolv_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))))))); definitionlet "G", "H" be ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); let "A" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "g" :::".:"::: "A" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "H" equals :: GRSOLV_1:def 3 (Set ($#k10_group_6 :::"Image"::: ) (Set "(" "g" ($#k1_grsolv_1 :::"|"::: ) "A" ")" )); end; :: deftheorem defines :::".:"::: GRSOLV_1:def 3 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "g")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k10_group_6 :::"Image"::: ) (Set "(" (Set (Var "g")) ($#k1_grsolv_1 :::"|"::: ) (Set (Var "A")) ")" )))))); theorem :: GRSOLV_1:8 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "g")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))))))) ; theorem :: GRSOLV_1:9 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k10_group_6 :::"Image"::: ) (Set "(" (Set (Var "h")) ($#k1_grsolv_1 :::"|"::: ) (Set (Var "A")) ")" )) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))))))) ; theorem :: GRSOLV_1:10 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))))))) ; theorem :: GRSOLV_1:11 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "H")))) & (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set "(" ($#k10_group_6 :::"Image"::: ) (Set (Var "h")) ")" ))) ")" ))) ; theorem :: GRSOLV_1:12 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "B")))) "holds" (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "B"))))))) ; theorem :: GRSOLV_1:13 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k13_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ))) ")" ))))) ; theorem :: GRSOLV_1:14 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GRSOLV_1:15 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "B")))) "holds" (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "B"))))))) ; theorem :: GRSOLV_1:16 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_grsolv_1 :::"solvable"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))) "is" ($#v1_grsolv_1 :::"solvable"::: ) ))) ;