let O be set ; for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2
let G be GroupWithOperators of O; for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2
let H1 be StableSubgroup of G; for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2
let N1, N2 be strict StableSubgroup of H1; for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2
let N19, N29 be strict StableSubgroup of G; ( N1 = N19 & N2 = N29 implies N19 * N29 = N1 * N2 )
set X = { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } ;
set Y = { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } ;
assume A1:
( N1 = N19 & N2 = N29 )
; N19 * N29 = N1 * N2
A2:
now for x being object st x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } holds
x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) }
N2 is
Subgroup of
H1
by Def7;
then A3:
the
carrier of
N2 c= the
carrier of
H1
by GROUP_2:def 5;
let x be
object ;
( x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } implies x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } )assume
x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) }
;
x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } then consider g,
h being
Element of
G such that A4:
x = g * h
and A5:
(
g in carr N19 &
h in carr N29 )
;
N1 is
Subgroup of
H1
by Def7;
then
the
carrier of
N1 c= the
carrier of
H1
by GROUP_2:def 5;
then reconsider g =
g,
h =
h as
Element of
H1 by A1, A5, A3;
x = g * h
by A4, Th3;
hence
x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) }
by A1, A5;
verum end;
hence
N19 * N29 = N1 * N2
by A2, TARSKI:2; verum