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 N1', N2' being strict StableSubgroup of G st N1 = N1' & N2 = N2' holds
N1' * N2' = N1 * N2
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N1', N2' being strict StableSubgroup of G st N1 = N1' & N2 = N2' holds
N1' * N2' = N1 * N2
let H1 be StableSubgroup of G; :: thesis: for N1, N2 being strict StableSubgroup of H1
for N1', N2' being strict StableSubgroup of G st N1 = N1' & N2 = N2' holds
N1' * N2' = N1 * N2
let N1, N2 be strict StableSubgroup of H1; :: thesis: for N1', N2' being strict StableSubgroup of G st N1 = N1' & N2 = N2' holds
N1' * N2' = N1 * N2
let N1', N2' be strict StableSubgroup of G; :: thesis: ( N1 = N1' & N2 = N2' implies N1' * N2' = N1 * N2 )
set X = { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) } ;
set Y = { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) } ;
assume A1: ( N1 = N1' & N2 = N2' ) ; :: thesis: N1' * N2' = N1 * N2

A2: now

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 set ; :: thesis: ( x in { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) } implies x in { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) } )
assume x in { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) } ; :: thesis: x in { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) }
then consider g, h being Element of such that
A4: x = g * h and
A5: ( g in carr N1' & h in carr N2' ) ;
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 by A1, A5, A3;
x = g * h by A4, Th3;
hence x in { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) } by A1, A5; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) } implies x in { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) } )
assume x in { (g * h) where g, h is Element of : ( g in carr N1 & h in carr N2 ) } ; :: thesis: x in { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) }
then consider g, h being Element of such that
A6: x = g * h and
A7: ( g in carr N1 & h in carr N2 ) ;
reconsider g = g, h = h as Element of by Th2;
x = g * h by A6, Th3;
hence x in { (g * h) where g, h is Element of : ( g in carr N1' & h in carr N2' ) } by A1, A7; :: thesis: verum

end;

hence N1' * N2' = N1 * N2 by A2, TARSKI:2; :: thesis: verum