let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: N19 * N29 = N1 * N2
A2: now :: thesis: 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 ; :: thesis: ( 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 ) } ; :: thesis: 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 ;
hence x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } by A1, A5; :: thesis: verum
end;
now :: thesis: for x being object st x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } holds
x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) }
let x be object ; :: thesis: ( x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } implies x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } )
assume x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } ; :: thesis: x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) }
then consider g, h being Element of H1 such that
A6: x = g * h and
A7: ( g in carr N1 & h in carr N2 ) ;
reconsider g = g, h = h as Element of G by Th2;
x = g * h by ;
hence x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } by A1, A7; :: thesis: verum
end;
hence N19 * N29 = N1 * N2 by ; :: thesis: verum