let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let H1 be StableSubgroup of G; :: thesis:
let N1, N2 be strict StableSubgroup of H1; :: thesis:
let N19, N29 be strict StableSubgroup of G; :: thesis:
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:

A2: now :: thesis:

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:
assume x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } ; :: thesis:
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; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume x in { (g * h) where g, h is Element of H1 : ( g in carr N1 & h in carr N2 ) } ; :: thesis:
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 A6, Th3;
hence x in { (g * h) where g, h is Element of G : ( g in carr N19 & h in carr N29 ) } by A1, A7; :: thesis:

end;

hence N19 * N29 = N1 * N2 by A2, TARSKI:2; :: thesis: