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

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 ) }

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 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: verum

end;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 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: verum

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 ) }

hence
N19 * N29 = N1 * N2
by A2, TARSKI:2; :: thesis: verumx 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 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: verum

end;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 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: verum