:: GROUP_11 semantic presentation

K92() is Element of K19(K88())
K88() is set
K19(K88()) is set
K87() is set
K19(K87()) is set
K19(K92()) is set
2 is non empty set
K20(2,2) is set
K20(K20(2,2),2) is set
K19(K20(K20(2,2),2)) is set
K91() is set
{} is empty set
the empty set is empty set
1 is non empty set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() normal Subgroup of G
N1 is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N1 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N1) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in carr N ) } is set
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
(N1 * N) * (N2 * N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N1 * N & b₂ in N2 * N ) } is set
N1 * N2 is Element of the carrier of G
(N1 * N2) * N is Element of K19( the carrier of G)
(N1 * N2) * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,(N1 * N2)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N1 * N2)) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N1 * N2)) & b₂ in carr N ) } is set
(N1 * N) * N2 is Element of K19( the carrier of G)
(N1 * N) * K158( the carrier of G,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N1 * N & b₂ in K158( the carrier of G,N2) ) } is set
((N1 * N) * N2) * N is Element of K19( the carrier of G)
((N1 * N) * N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (N1 * N) * N2 & b₂ in carr N ) } is set
N * N2 is Element of K19( the carrier of G)
(carr N) * N2 is Element of K19( the carrier of G)
(carr N) * K158( the carrier of G,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in K158( the carrier of G,N2) ) } is set
N1 * (N * N2) is Element of K19( the carrier of G)
K158( the carrier of G,N1) * (N * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in N * N2 ) } is set
(N1 * (N * N2)) * N is Element of K19( the carrier of G)
(N1 * (N * N2)) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N1 * (N * N2) & b₂ in carr N ) } is set
N1 * (N2 * N) is Element of K19( the carrier of G)
K158( the carrier of G,N1) * (N2 * N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in N2 * N ) } is set
(N1 * (N2 * N)) * N is Element of K19( the carrier of G)
(N1 * (N2 * N)) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N1 * (N2 * N) & b₂ in carr N ) } is set
((N1 * N2) * N) * N is Element of K19( the carrier of G)
((N1 * N2) * N) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (N1 * N2) * N & b₂ in carr N ) } is set
N * N is Element of K19( the carrier of G)
(carr N) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N ) } is set
(N1 * N2) * (N * N) is Element of K19( the carrier of G)
K158( the carrier of G,(N1 * N2)) * (N * N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N1 * N2)) & b₂ in N * N ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N2 is Element of the carrier of G
N1 is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N1 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N1) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in carr N ) } is set
N2 * N is Element of K19( the carrier of G)
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
carr N1 is Element of K19( the carrier of G)
K19( the carrier of G) is set
the carrier of N1 is non empty set
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
N3 is set
N4 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N1 is Element of the carrier of G
N is Element of the carrier of G
N * N1 is Element of the carrier of G
N " is Element of the carrier of G
(N * N1) * (N ") is Element of the carrier of G
N2 is non empty unital Group-like V103() normal Subgroup of G
N * N2 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N) & b₂ in carr N2 ) } is set
N2 * N is Element of K19( the carrier of G)
(carr N2) * N is Element of K19( the carrier of G)
(carr N2) * K158( the carrier of G,N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in K158( the carrier of G,N) ) } is set
N3 is Element of the carrier of G
N3 * N is Element of the carrier of G
N * (N ") is Element of the carrier of G
N3 * (N * (N ")) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
N3 * (1_ G) is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N1 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N1) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in carr N ) } is set
N * N1 is Element of K19( the carrier of G)
(carr N) * N1 is Element of K19( the carrier of G)
(carr N) * K158( the carrier of G,N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in K158( the carrier of G,N1) ) } is set
N2 is set
N3 is Element of the carrier of G
N4 is Element of the carrier of G
N1 * N4 is Element of the carrier of G
N1 " is Element of the carrier of G
(N1 * N4) * (N1 ") is Element of the carrier of G
((N1 * N4) * (N1 ")) * N1 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N * N1 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(carr N) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N1 ) } is set
N2 is Element of the carrier of G
N3 is Element of the carrier of G
N4 is Element of the carrier of G
N3 * N4 is Element of the carrier of G
N3 is Element of the carrier of G
N4 is Element of the carrier of G
N3 * N4 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
N is non empty strict unital Group-like V103() normal Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N * N1 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(carr N) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N1 ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * (1_ G) is Element of the carrier of G
N2 is Element of the carrier of G
N3 is Element of the carrier of G
N2 * N3 is Element of the carrier of G
N4 is Element of the carrier of G
y is Element of the carrier of G
N4 * y is Element of the carrier of G
z is Element of the carrier of G
z9 is Element of the carrier of G
z * z9 is Element of the carrier of G
(N4 * y) * z is Element of the carrier of G
((N4 * y) * z) * z9 is Element of the carrier of G
y * z is Element of the carrier of G
N4 * (y * z) is Element of the carrier of G
(N4 * (y * z)) * z9 is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
(carr N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N ) } is set
y is Element of the carrier of G
a is Element of the carrier of G
y * a is Element of the carrier of G
N4 * y is Element of the carrier of G
(N4 * y) * a is Element of the carrier of G
((N4 * y) * a) * z9 is Element of the carrier of G
a * z9 is Element of the carrier of G
(N4 * y) * (a * z9) is Element of the carrier of G
N2 is Element of the carrier of G
N2 " is Element of the carrier of G
N3 is Element of the carrier of G
N4 is Element of the carrier of G
N3 * N4 is Element of the carrier of G
N4 " is Element of the carrier of G
N3 " is Element of the carrier of G
(N4 ") * (N3 ") is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
(carr N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N ) } is set
G is non empty unital Group-like V103() L8()
N is non empty strict unital Group-like V103() normal Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N * N1 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(carr N) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N1 ) } is set
N2 is non empty strict unital Group-like V103() Subgroup of G
the carrier of N2 is non empty set
N4 is Element of the carrier of G
N3 is Element of the carrier of G
N3 * N4 is Element of the carrier of G
N3 " is Element of the carrier of G
(N3 * N4) * (N3 ") is Element of the carrier of G
y is Element of the carrier of G
z is Element of the carrier of G
y * z is Element of the carrier of G
N3 * y is Element of the carrier of G
(N3 * y) * z is Element of the carrier of G
((N3 * y) * z) * (N3 ") is Element of the carrier of G
z * (N3 ") is Element of the carrier of G
(N3 * y) * (z * (N3 ")) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(N3 * y) * (1_ G) is Element of the carrier of G
((N3 * y) * (1_ G)) * (z * (N3 ")) is Element of the carrier of G
(N3 ") * N3 is Element of the carrier of G
(N3 * y) * ((N3 ") * N3) is Element of the carrier of G
((N3 * y) * ((N3 ") * N3)) * (z * (N3 ")) is Element of the carrier of G
(N3 * y) * (N3 ") is Element of the carrier of G
((N3 * y) * (N3 ")) * N3 is Element of the carrier of G
(((N3 * y) * (N3 ")) * N3) * (z * (N3 ")) is Element of the carrier of G
N3 * (z * (N3 ")) is Element of the carrier of G
((N3 * y) * (N3 ")) * (N3 * (z * (N3 "))) is Element of the carrier of G
N3 * z is Element of the carrier of G
(N3 * z) * (N3 ") is Element of the carrier of G
((N3 * y) * (N3 ")) * ((N3 * z) * (N3 ")) is Element of the carrier of G
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
the carrier of N is non empty set
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
N3 is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
N3 * (1_ G) is Element of the carrier of G
N3 is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * N3 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() normal Subgroup of G
the carrier of N is non empty set
N1 is non empty unital Group-like V103() normal Subgroup of G
N2 is non empty unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
(N3 * N1) * (N4 * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N3 * N1 & b₂ in N4 * N2 ) } is set
N3 * N4 is Element of the carrier of G
(N3 * N4) * N is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
(N3 * N4) * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,(N3 * N4)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N3 * N4)) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N3 * N4)) & b₂ in carr N ) } is set
(N3 * N1) * N4 is Element of K19( the carrier of G)
(N3 * N1) * K158( the carrier of G,N4) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N3 * N1 & b₂ in K158( the carrier of G,N4) ) } is set
((N3 * N1) * N4) * N2 is Element of K19( the carrier of G)
((N3 * N1) * N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (N3 * N1) * N4 & b₂ in carr N2 ) } is set
N1 * N4 is Element of K19( the carrier of G)
(carr N1) * N4 is Element of K19( the carrier of G)
(carr N1) * K158( the carrier of G,N4) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in K158( the carrier of G,N4) ) } is set
N3 * (N1 * N4) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * (N1 * N4) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in N1 * N4 ) } is set
(N3 * (N1 * N4)) * N2 is Element of K19( the carrier of G)
(N3 * (N1 * N4)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N3 * (N1 * N4) & b₂ in carr N2 ) } is set
N4 * N1 is Element of K19( the carrier of G)
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
N3 * (N4 * N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * (N4 * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in N4 * N1 ) } is set
(N3 * (N4 * N1)) * N2 is Element of K19( the carrier of G)
(N3 * (N4 * N1)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N3 * (N4 * N1) & b₂ in carr N2 ) } is set
(N3 * N4) * N1 is Element of K19( the carrier of G)
(N3 * N4) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N3 * N4)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N3 * N4)) & b₂ in carr N1 ) } is set
((N3 * N4) * N1) * N2 is Element of K19( the carrier of G)
((N3 * N4) * N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (N3 * N4) * N1 & b₂ in carr N2 ) } is set
(N3 * N4) * (N1 * N2) is Element of K19( the carrier of G)
K158( the carrier of G,(N3 * N4)) * (N1 * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N3 * N4)) & b₂ in N1 * N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() normal Subgroup of G
carr N is Element of K19( the carrier of G)
K19( the carrier of G) is set
the carrier of N is non empty set
N1 is Element of the carrier of G
N1 " is Element of the carrier of G
N1 * N is Element of K19( the carrier of G)
N1 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N1) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N1) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N1) & b₂ in carr N ) } is set
(N1 * N) * (N1 ") is Element of K19( the carrier of G)
K158( the carrier of G,(N1 ")) is non empty Element of K19( the carrier of G)
(N1 * N) * K158( the carrier of G,(N1 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N1 * N & b₂ in K158( the carrier of G,(N1 ")) ) } is set
N * N1 is Element of K19( the carrier of G)
(carr N) * N1 is Element of K19( the carrier of G)
(carr N) * K158( the carrier of G,N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in K158( the carrier of G,N1) ) } is set
(N * N1) * (N1 ") is Element of K19( the carrier of G)
(N * N1) * K158( the carrier of G,(N1 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N * N1 & b₂ in K158( the carrier of G,(N1 ")) ) } is set
N1 * (N1 ") is Element of the carrier of G
N * (N1 * (N1 ")) is Element of K19( the carrier of G)
(carr N) * (N1 * (N1 ")) is Element of K19( the carrier of G)
K158( the carrier of G,(N1 * (N1 "))) is non empty Element of K19( the carrier of G)
(carr N) * K158( the carrier of G,(N1 * (N1 "))) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in K158( the carrier of G,(N1 * (N1 "))) ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
N * (1_ G) is Element of K19( the carrier of G)
(carr N) * (1_ G) is Element of K19( the carrier of G)
K158( the carrier of G,(1_ G)) is non empty Element of K19( the carrier of G)
(carr N) * K158( the carrier of G,(1_ G)) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in K158( the carrier of G,(1_ G)) ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N1 is non empty unital Group-like V103() Subgroup of G
N is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N1 is non empty unital Group-like V103() Subgroup of G
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N is non empty Element of K19( the carrier of G)
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N1 is non empty unital Group-like V103() Subgroup of G
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N is non empty Element of K19( the carrier of G)
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N \/ N1 is non empty Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,(N \/ N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N \/ N1 } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N1 } is set
(G,N,N2) \/ (G,N1,N2) is Element of K19( the carrier of G)
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N /\ N1 is Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,(N /\ N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N /\ N1 } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N1 } is set
(G,N,N2) /\ (G,N1,N2) is Element of K19( the carrier of G)
N3 is set
N4 is Element of the carrier of G
y is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
N4 * N2 is Element of K19( the carrier of G)
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N1 } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N1 } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N \/ N1 is non empty Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N1 } is set
(G,N,N2) \/ (G,N1,N2) is Element of K19( the carrier of G)
(G,(N \/ N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N \/ N1 } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
N4 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N \/ N1 is non empty Element of K19( the carrier of G)
N2 is non empty unital Group-like V103() Subgroup of G
(G,(N \/ N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N \/ N1 } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N1 } is set
(G,N,N2) \/ (G,N1,N2) is Element of K19( the carrier of G)
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
N3 is set
N4 is Element of the carrier of G
N4 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
N3 is set
N4 is Element of the carrier of G
N4 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N * N1 is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N & b₂ in N1 ) } is set
N2 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N1 } is set
(G,N,N2) * (G,N1,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in (G,N1,N2) ) } is set
(G,(N * N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N * N1 } is set
N3 is set
N4 is Element of the carrier of G
y is Element of the carrier of G
z is Element of the carrier of G
y * z is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
z * N2 is Element of K19( the carrier of G)
z * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N2 ) } is set
(y * N2) * (z * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in z * N2 ) } is set
(y * z) * N2 is Element of K19( the carrier of G)
(y * z) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * z)) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N * N1 is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N & b₂ in N1 ) } is set
N2 is non empty unital Group-like V103() Subgroup of G
(G,(N * N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N * N1 } is set
N3 is Element of the carrier of G
N3 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N3 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N2 ) } is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty Element of K19( the carrier of G)
N * N1 is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N & b₂ in N1 ) } is set
N2 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N1 } is set
(G,N,N2) * (G,N1,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in (G,N1,N2) ) } is set
(G,(N * N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N * N1 } is set
N3 is set
N4 is Element of the carrier of G
y is Element of the carrier of G
z is Element of the carrier of G
y * z is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
z * N2 is Element of K19( the carrier of G)
z * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N2 ) } is set
z9 is set
y is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
(y * N2) * (z * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in z * N2 ) } is set
(y * z) * N2 is Element of K19( the carrier of G)
(y * z) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * z)) & b₂ in carr N2 ) } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
y is set
z is Element of the carrier of G
z9 is Element of the carrier of G
y is Element of the carrier of G
z9 * y is Element of the carrier of G
(z9 * y) * N2 is Element of K19( the carrier of G)
(z9 * y) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(z9 * y)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(z9 * y)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(z9 * y)) & b₂ in carr N2 ) } is set
z9 * N2 is Element of K19( the carrier of G)
z9 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N2 ) } is set
y * N2 is Element of K19( the carrier of G)
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
(z9 * N2) * (y * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in z9 * N2 & b₂ in y * N2 ) } is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
a * N2 is Element of K19( the carrier of G)
a * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,a) is non empty Element of K19( the carrier of G)
K158( the carrier of G,a) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,a) & b₂ in carr N2 ) } is set
b * N2 is Element of K19( the carrier of G)
b * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
(G,(G,(G,N,N1),N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,(G,N,N1),N1) } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
(G,(G,(G,N,N1),N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,(G,N,N1),N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
(G,(G,(G,N,N1),N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,(G,N,N1),N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
(G,(G,(G,N,N1),N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,(G,N,N1),N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
N2 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
z is set
z9 is Element of the carrier of G
z9 * N1 is Element of K19( the carrier of G)
z9 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses (G,N,N1) } is set
(G,(G,N,N1),N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= (G,N,N1) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
N4 is set
y is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
z is set
z9 is Element of the carrier of G
z9 * N1 is Element of K19( the carrier of G)
z9 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N1 ) } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
N3 is non empty unital Group-like V103() Subgroup of G
N2 /\ N3 is non empty strict unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses N } is set
(G,N,N2) /\ (G,N,N3) is Element of K19( the carrier of G)
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
N3 is non empty unital Group-like V103() Subgroup of G
N2 /\ N3 is non empty strict unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= N } is set
(G,N,N2) /\ (G,N,N3) is Element of K19( the carrier of G)
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N } is set
(G,N,N1) /\ (G,N,N2) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= N } is set
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N,N1) \/ (G,N,N2) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses N } is set
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
K19( the carrier of G) is set
N is non empty Element of K19( the carrier of G)
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses N } is set
(G,N,N1) * N2 is Element of K19( the carrier of G)
(G,N,N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N1) & b₂ in carr N2 ) } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N } is set
(G,N,N2) * N1 is Element of K19( the carrier of G)
(G,N,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in carr N1 ) } is set
((G,N,N1) * N2) /\ ((G,N,N2) * N1) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses N } is set
N4 is set
y is Element of the carrier of G
y * N3 is Element of K19( the carrier of G)
carr N3 is Element of K19( the carrier of G)
y * (carr N3) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N3 ) } is set
z is set
z9 is Element of the carrier of G
y is Element of the carrier of G
y * y is Element of the carrier of G
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
y * a is Element of the carrier of G
(y * a) * b is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
(y * N1) * b is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
(y * N1) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N1 & b₂ in K158( the carrier of G,b) ) } is set
N1 * b is Element of K19( the carrier of G)
(carr N1) * b is Element of K19( the carrier of G)
(carr N1) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in K158( the carrier of G,b) ) } is set
y * (N1 * b) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (N1 * b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in N1 * b ) } is set
b * N1 is Element of K19( the carrier of G)
b * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N1 ) } is set
y * (b * N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (b * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in b * N1 ) } is set
y * b is Element of the carrier of G
(y * b) * N1 is Element of K19( the carrier of G)
(y * b) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * b)) & b₂ in carr N1 ) } is set
b " is Element of the carrier of G
(y * b) * (b ") is Element of the carrier of G
b * (b ") is Element of the carrier of G
y * (b * (b ")) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
y * (1_ G) is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
(carr N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in carr N1 ) } is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
y * a is Element of the carrier of G
(y * a) * b is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
(y * N2) * b is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
(y * N2) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in K158( the carrier of G,b) ) } is set
N2 * b is Element of K19( the carrier of G)
(carr N2) * b is Element of K19( the carrier of G)
(carr N2) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in K158( the carrier of G,b) ) } is set
y * (N2 * b) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (N2 * b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in N2 * b ) } is set
b * N2 is Element of K19( the carrier of G)
b * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N2 ) } is set
y * (b * N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (b * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in b * N2 ) } is set
y * b is Element of the carrier of G
(y * b) * N2 is Element of K19( the carrier of G)
(y * b) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * b)) & b₂ in carr N2 ) } is set
b " is Element of the carrier of G
(y * b) * (b ") is Element of the carrier of G
b * (b ") is Element of the carrier of G
y * (b * (b ")) is Element of the carrier of G
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N1 is non empty unital Group-like V103() Subgroup of G
N is non empty unital Group-like V103() Subgroup of G
carr N is Element of K19( the carrier of G)
K19( the carrier of G) is set
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
N2 is set
N3 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
N3 is Element of the carrier of G
N3 * N is Element of K19( the carrier of G)
N3 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
N1 is non empty unital Group-like V103() Subgroup of G
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(G,N1,N) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N1 } is set
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
N3 is Element of the carrier of G
N3 * N is Element of K19( the carrier of G)
N3 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N2 is Element of the carrier of G
N2 * N is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N2 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N ) } is set
N1 is non empty unital Group-like V103() Subgroup of G
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(G,N1,N) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N1 } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
N2 is set
N3 is Element of the carrier of G
N3 * N is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
N3 * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
carr N is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
the carrier of N is non empty set
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
N2 is set
N3 is Element of the carrier of N
N4 is Element of the carrier of G
N4 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
(G,N1,N) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N1 } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N1,N2) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N1 } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
N3 is set
N4 is Element of the carrier of G
N4 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
(G,N,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N } is set
N1 is non empty unital Group-like V103() Subgroup of G
(G,N1,N1) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N1 } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N1,N2) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N1 } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
N3 is set
N4 is Element of the carrier of G
N4 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
(G,N1,N) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
(G,N1,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N1 } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N * N1 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(carr N) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N1 ) } is set
N2 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N1 } is set
(G,N,N2) * (G,N1,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in (G,N1,N2) ) } is set
(G,(N * N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= N * N1 } is set
N3 is set
N4 is Element of the carrier of G
y is Element of the carrier of G
z is Element of the carrier of G
y * z is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
z * N2 is Element of K19( the carrier of G)
z * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N2 ) } is set
(y * N2) * (z * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in z * N2 ) } is set
(y * z) * N2 is Element of K19( the carrier of G)
(y * z) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * z)) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N * N1 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(carr N) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N1 ) } is set
N2 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N1 } is set
(G,N,N2) * (G,N1,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in (G,N1,N2) ) } is set
(G,(N * N1),N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses N * N1 } is set
N3 is set
N4 is Element of the carrier of G
y is Element of the carrier of G
z is Element of the carrier of G
y * z is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
z * N2 is Element of K19( the carrier of G)
z * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N2 ) } is set
z9 is set
y is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
(y * N2) * (z * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in z * N2 ) } is set
(y * z) * N2 is Element of K19( the carrier of G)
(y * z) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * z)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * z)) & b₂ in carr N2 ) } is set
N3 is set
N4 is Element of the carrier of G
N4 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
N4 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N2 ) } is set
y is set
z is Element of the carrier of G
z9 is Element of the carrier of G
y is Element of the carrier of G
z9 * y is Element of the carrier of G
(z9 * y) * N2 is Element of K19( the carrier of G)
(z9 * y) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(z9 * y)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(z9 * y)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(z9 * y)) & b₂ in carr N2 ) } is set
z9 * N2 is Element of K19( the carrier of G)
z9 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N2 ) } is set
y * N2 is Element of K19( the carrier of G)
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
(z9 * N2) * (y * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in z9 * N2 & b₂ in y * N2 ) } is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
a * N2 is Element of K19( the carrier of G)
a * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,a) is non empty Element of K19( the carrier of G)
K158( the carrier of G,a) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,a) & b₂ in carr N2 ) } is set
b * N2 is Element of K19( the carrier of G)
b * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N2 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
N3 is non empty unital Group-like V103() Subgroup of G
N2 /\ N3 is non empty strict unital Group-like V103() Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
(G,N,N2) /\ (G,N,N3) is Element of K19( the carrier of G)
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() Subgroup of G
N2 is non empty unital Group-like V103() Subgroup of G
N3 is non empty unital Group-like V103() Subgroup of G
N2 /\ N3 is non empty strict unital Group-like V103() Subgroup of G
(G,N,N2) is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
(G,N,N2) /\ (G,N,N3) is Element of K19( the carrier of G)
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N,N1) /\ (G,N,N2) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
N4 is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N,N1) \/ (G,N,N2) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
N4 is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N,N1) * (G,N,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N1) & b₂ in (G,N,N2) ) } is set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
N4 is set
y is Element of the carrier of G
z is Element of the carrier of G
z9 is Element of the carrier of G
z * z9 is Element of the carrier of G
z * N1 is Element of K19( the carrier of G)
z * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N1 ) } is set
z9 * N2 is Element of K19( the carrier of G)
z9 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N2 ) } is set
(z * N1) * (z9 * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in z * N1 & b₂ in z9 * N2 ) } is set
(carr N) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N ) } is set
(z * z9) * N3 is Element of K19( the carrier of G)
carr N3 is Element of K19( the carrier of G)
(z * z9) * (carr N3) is Element of K19( the carrier of G)
K158( the carrier of G,(z * z9)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(z * z9)) * (carr N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(z * z9)) & b₂ in carr N3 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N,N1) * (G,N,N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N1) & b₂ in (G,N,N2) ) } is set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
N4 is set
y is Element of the carrier of G
z is Element of the carrier of G
z9 is Element of the carrier of G
z * z9 is Element of the carrier of G
z * N1 is Element of K19( the carrier of G)
z * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N1 ) } is set
z9 * N2 is Element of K19( the carrier of G)
z9 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,z9) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z9) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z9) & b₂ in carr N2 ) } is set
y is set
a is set
b is Element of the carrier of G
a is Element of the carrier of G
b * a is Element of the carrier of G
(carr N) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N ) } is set
(z * N1) * (z9 * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in z * N1 & b₂ in z9 * N2 ) } is set
(z * z9) * N3 is Element of K19( the carrier of G)
carr N3 is Element of K19( the carrier of G)
(z * z9) * (carr N3) is Element of K19( the carrier of G)
K158( the carrier of G,(z * z9)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(z * z9)) * (carr N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(z * z9)) & b₂ in carr N3 ) } is set
G is non empty unital Group-like V103() L8()
the carrier of G is non empty set
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty strict unital Group-like V103() normal Subgroup of G
N2 is non empty strict unital Group-like V103() normal Subgroup of G
N1 * N2 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
(carr N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in carr N2 ) } is set
(G,N,N1) is Element of K19( the carrier of G)
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N1) * N2 is Element of K19( the carrier of G)
(G,N,N1) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N1) & b₂ in carr N2 ) } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N,N2) * N1 is Element of K19( the carrier of G)
(G,N,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,N,N2) & b₂ in carr N1 ) } is set
((G,N,N1) * N2) /\ ((G,N,N2) * N1) is Element of K19( the carrier of G)
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
N4 is set
y is Element of the carrier of G
y * N3 is Element of K19( the carrier of G)
carr N3 is Element of K19( the carrier of G)
y * (carr N3) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N3 ) } is set
z is set
z9 is Element of the carrier of G
y is Element of the carrier of G
y * y is Element of the carrier of G
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
y * a is Element of the carrier of G
(y * a) * b is Element of the carrier of G
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
(y * N1) * b is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
(y * N1) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N1 & b₂ in K158( the carrier of G,b) ) } is set
N1 * b is Element of K19( the carrier of G)
(carr N1) * b is Element of K19( the carrier of G)
(carr N1) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in K158( the carrier of G,b) ) } is set
y * (N1 * b) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (N1 * b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in N1 * b ) } is set
b * N1 is Element of K19( the carrier of G)
b * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N1 ) } is set
y * (b * N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (b * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in b * N1 ) } is set
y * b is Element of the carrier of G
(y * b) * N1 is Element of K19( the carrier of G)
(y * b) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * b)) & b₂ in carr N1 ) } is set
b " is Element of the carrier of G
(y * b) * (b ") is Element of the carrier of G
b * (b ") is Element of the carrier of G
y * (b * (b ")) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
y * (1_ G) is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
(carr N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in carr N1 ) } is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
y * a is Element of the carrier of G
(y * a) * b is Element of the carrier of G
y * N2 is Element of K19( the carrier of G)
y * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N2 ) } is set
(y * N2) * b is Element of K19( the carrier of G)
K158( the carrier of G,b) is non empty Element of K19( the carrier of G)
(y * N2) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in y * N2 & b₂ in K158( the carrier of G,b) ) } is set
N2 * b is Element of K19( the carrier of G)
(carr N2) * b is Element of K19( the carrier of G)
(carr N2) * K158( the carrier of G,b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in K158( the carrier of G,b) ) } is set
y * (N2 * b) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (N2 * b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in N2 * b ) } is set
b * N2 is Element of K19( the carrier of G)
b * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,b) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,b) & b₂ in carr N2 ) } is set
y * (b * N2) is Element of K19( the carrier of G)
K158( the carrier of G,y) * (b * N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in b * N2 ) } is set
y * b is Element of the carrier of G
(y * b) * N2 is Element of K19( the carrier of G)
(y * b) * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(y * b)) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(y * b)) & b₂ in carr N2 ) } is set
b " is Element of the carrier of G
(y * b) * (b ") is Element of the carrier of G
b * (b ") is Element of the carrier of G
y * (b * (b ")) is Element of the carrier of G
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(1_ G) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(1_ G)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(1_ G)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(1_ G)) & b₂ in carr N1 ) } is set
N2 is Element of the carrier of G
N3 is Element of the carrier of G
N2 * N3 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N4 is Element of the carrier of G
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
y is Element of the carrier of G
(N2 * N1) * (N3 * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N2 * N1 & b₂ in N3 * N1 ) } is set
(N2 * N3) * N1 is Element of K19( the carrier of G)
(N2 * N3) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N2 * N3)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N2 * N3)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N2 * N3)) & b₂ in carr N1 ) } is set
N4 * N1 is Element of K19( the carrier of G)
N4 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N4) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N4) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N4) & b₂ in carr N1 ) } is set
y * N1 is Element of K19( the carrier of G)
y * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,y) is non empty Element of K19( the carrier of G)
K158( the carrier of G,y) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,y) & b₂ in carr N1 ) } is set
(N4 * N1) * (y * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N4 * N1 & b₂ in y * N1 ) } is set
N4 * y is Element of the carrier of G
(N4 * y) * N1 is Element of K19( the carrier of G)
(N4 * y) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N4 * y)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N4 * y)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N4 * y)) & b₂ in carr N1 ) } is set
N2 is Element of the carrier of G
N2 " is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 is Element of the carrier of G
N4 is Element of the carrier of G
N2 * N4 is Element of the carrier of G
N4 " is Element of the carrier of G
N3 " is Element of the carrier of G
(N4 ") * (N2 ") is Element of the carrier of G
N1 * (N2 ") is Element of K19( the carrier of G)
(carr N1) * (N2 ") is Element of K19( the carrier of G)
K158( the carrier of G,(N2 ")) is non empty Element of K19( the carrier of G)
(carr N1) * K158( the carrier of G,(N2 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in K158( the carrier of G,(N2 ")) ) } is set
(N2 ") * N1 is Element of K19( the carrier of G)
(N2 ") * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N2 ")) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N2 ")) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() Subgroup of G
N1 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
(1_ G) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(1_ G)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(1_ G)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(1_ G)) & b₂ in carr N1 ) } is set
N2 is Element of the carrier of G
N3 is Element of the carrier of G
N2 * N3 is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
N3 * N1 is Element of K19( the carrier of G)
N3 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N1 ) } is set
(N2 * N1) * (N3 * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N2 * N1 & b₂ in N3 * N1 ) } is set
(carr N) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N & b₂ in carr N ) } is set
(N2 * N3) * N1 is Element of K19( the carrier of G)
(N2 * N3) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N2 * N3)) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N2 * N3)) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N2 * N3)) & b₂ in carr N1 ) } is set
N2 is Element of the carrier of G
N2 " is Element of the carrier of G
N2 * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
N2 * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,N2) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N2) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N2) & b₂ in carr N1 ) } is set
(N2 ") * N is Element of K19( the carrier of G)
(N2 ") * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,(N2 ")) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N2 ")) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N2 ")) & b₂ in carr N ) } is set
(N2 ") * N1 is Element of K19( the carrier of G)
(N2 ") * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N2 ")) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N2 ")) & b₂ in carr N1 ) } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() normal Subgroup of G
N1 is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
N2 is non empty strict unital Group-like V103() Subgroup of G
the carrier of N2 is non empty set
N3 is Element of the carrier of G
N3 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
N3 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N2 ) } is set
N2 * N3 is Element of K19( the carrier of G)
(carr N2) * N3 is Element of K19( the carrier of G)
(carr N2) * K158( the carrier of G,N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in K158( the carrier of G,N3) ) } is set
N4 is set
y is Element of the carrier of G
z is Element of the carrier of G
N3 * z is Element of the carrier of G
z * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
z * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N1 ) } is set
z9 is Element of the carrier of G
N3 * z9 is Element of the carrier of G
N3 " is Element of the carrier of G
(N3 * z9) * (N3 ") is Element of the carrier of G
N3 * (z * N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * (z * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in z * N1 ) } is set
(N3 * (z * N1)) * (N3 ") is Element of K19( the carrier of G)
K158( the carrier of G,(N3 ")) is non empty Element of K19( the carrier of G)
(N3 * (z * N1)) * K158( the carrier of G,(N3 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in N3 * (z * N1) & b₂ in K158( the carrier of G,(N3 ")) ) } is set
(z * N1) * (N3 ") is Element of K19( the carrier of G)
(z * N1) * K158( the carrier of G,(N3 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in z * N1 & b₂ in K158( the carrier of G,(N3 ")) ) } is set
N3 * ((z * N1) * (N3 ")) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * ((z * N1) * (N3 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in (z * N1) * (N3 ") ) } is set
N1 * (N3 ") is Element of K19( the carrier of G)
(carr N1) * (N3 ") is Element of K19( the carrier of G)
(carr N1) * K158( the carrier of G,(N3 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N1 & b₂ in K158( the carrier of G,(N3 ")) ) } is set
z * (N1 * (N3 ")) is Element of K19( the carrier of G)
K158( the carrier of G,z) * (N1 * (N3 ")) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in N1 * (N3 ") ) } is set
N3 * (z * (N1 * (N3 "))) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * (z * (N1 * (N3 "))) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in z * (N1 * (N3 ")) ) } is set
(N3 ") * N1 is Element of K19( the carrier of G)
(N3 ") * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N3 ")) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N3 ")) & b₂ in carr N1 ) } is set
z * ((N3 ") * N1) is Element of K19( the carrier of G)
K158( the carrier of G,z) * ((N3 ") * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in (N3 ") * N1 ) } is set
N3 * (z * ((N3 ") * N1)) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * (z * ((N3 ") * N1)) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in z * ((N3 ") * N1) ) } is set
z * (N3 ") is Element of the carrier of G
(z * (N3 ")) * N1 is Element of K19( the carrier of G)
(z * (N3 ")) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(z * (N3 "))) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(z * (N3 "))) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(z * (N3 "))) & b₂ in carr N1 ) } is set
N3 * ((z * (N3 ")) * N1) is Element of K19( the carrier of G)
K158( the carrier of G,N3) * ((z * (N3 ")) * N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in (z * (N3 ")) * N1 ) } is set
N3 * (z * (N3 ")) is Element of the carrier of G
(N3 * (z * (N3 "))) * N1 is Element of K19( the carrier of G)
(N3 * (z * (N3 "))) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,(N3 * (z * (N3 ")))) is non empty Element of K19( the carrier of G)
K158( the carrier of G,(N3 * (z * (N3 ")))) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,(N3 * (z * (N3 ")))) & b₂ in carr N1 ) } is set
(N3 * z) * (N3 ") is Element of the carrier of G
((N3 * z) * (N3 ")) * N1 is Element of K19( the carrier of G)
((N3 * z) * (N3 ")) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,((N3 * z) * (N3 "))) is non empty Element of K19( the carrier of G)
K158( the carrier of G,((N3 * z) * (N3 "))) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,((N3 * z) * (N3 "))) & b₂ in carr N1 ) } is set
((N3 * z) * (N3 ")) * N3 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty strict unital Group-like V103() Subgroup of G
the carrier of N2 is non empty set
N3 is Element of the carrier of G
N3 * N2 is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
N3 * (carr N2) is Element of K19( the carrier of G)
K158( the carrier of G,N3) is non empty Element of K19( the carrier of G)
K158( the carrier of G,N3) * (carr N2) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,N3) & b₂ in carr N2 ) } is set
N2 * N3 is Element of K19( the carrier of G)
(carr N2) * N3 is Element of K19( the carrier of G)
(carr N2) * K158( the carrier of G,N3) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr N2 & b₂ in K158( the carrier of G,N3) ) } is set
N4 is set
y is Element of the carrier of G
z is Element of the carrier of G
N3 * z is Element of the carrier of G
z * N1 is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
z * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,z) is non empty Element of K19( the carrier of G)
K158( the carrier of G,z) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,z) & b₂ in carr N1 ) } is set
N3 " is Element of the carrier of G
(N3 * z) * (N3 ") is Element of the carrier of G
((N3 * z) * (N3 ")) * N is Element of K19( the carrier of G)
((N3 * z) * (N3 ")) * (carr N) is Element of K19( the carrier of G)
K158( the carrier of G,((N3 * z) * (N3 "))) is non empty Element of K19( the carrier of G)
K158( the carrier of G,((N3 * z) * (N3 "))) * (carr N) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,((N3 * z) * (N3 "))) & b₂ in carr N ) } is set
((N3 * z) * (N3 ")) * N1 is Element of K19( the carrier of G)
((N3 * z) * (N3 ")) * (carr N1) is Element of K19( the carrier of G)
K158( the carrier of G,((N3 * z) * (N3 "))) * (carr N1) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K158( the carrier of G,((N3 * z) * (N3 "))) & b₂ in carr N1 ) } is set
((N3 * z) * (N3 ")) * N3 is Element of the carrier of G
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N1) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N1 misses carr N } is set
(G,N,N1) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N1 c= carr N } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N } is set
(G,N,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N } is set
(G,N,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N3 c= carr N } is set
G is non empty unital Group-like V103() L8()
N1 is non empty unital Group-like V103() normal Subgroup of G
N2 is non empty unital Group-like V103() normal Subgroup of G
N is non empty unital Group-like V103() normal Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N1 } is set
(G,N2,N) is Element of K19( the carrier of G)
carr N2 is Element of K19( the carrier of G)
the carrier of N2 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N2 } is set
N3 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N3 is non empty set
N4 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N4 is non empty set
(G,N1,N3) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N3 misses carr N1 } is set
(G,N1,N4) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N4 misses carr N1 } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N } is set
N1 is non empty unital Group-like V103() normal Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ * N c= carr N1 } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : b₁ * N2 c= carr N1 } is set
G is non empty unital Group-like V103() L8()
N is non empty unital Group-like V103() normal Subgroup of G
(G,N,N) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is set
carr N is Element of K19( the carrier of G)
the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N } is set
N1 is non empty unital Group-like V103() normal Subgroup of G
(G,N1,N) is Element of K19( the carrier of G)
carr N1 is Element of K19( the carrier of G)
the carrier of N1 is non empty set
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N misses carr N1 } is set
N2 is non empty strict unital Group-like V103() normal Subgroup of G
the carrier of N2 is non empty set
(G,N1,N2) is Element of K19( the carrier of G)
{ b₁ where b₁ is Element of the carrier of G : not b₁ * N2 misses carr N1 } is set