let O be set ; :: thesis: for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds

the carrier of (H1 "\/" H2) = H1 * H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds

the carrier of (H1 "\/" H2) = H1 * H2

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 * H2 = H2 * H1 implies the carrier of (H1 "\/" H2) = H1 * H2 )

assume H1 * H2 = H2 * H1 ; :: thesis: the carrier of (H1 "\/" H2) = H1 * H2

then consider H being strict StableSubgroup of G such that

A1: the carrier of H = (carr H1) * (carr H2) by Th17;

then H is Subgroup of H1 "\/" H2 by Def7;

then A12: the carrier of H c= the carrier of (H1 "\/" H2) by GROUP_2:def 5;

(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)

then H1 "\/" H2 is Subgroup of H by Def7;

then the carrier of (H1 "\/" H2) c= the carrier of H by GROUP_2:def 5;

hence the carrier of (H1 "\/" H2) = H1 * H2 by A1, A12, XBOOLE_0:def 10; :: thesis: verum

for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds

the carrier of (H1 "\/" H2) = H1 * H2

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds

the carrier of (H1 "\/" H2) = H1 * H2

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 * H2 = H2 * H1 implies the carrier of (H1 "\/" H2) = H1 * H2 )

assume H1 * H2 = H2 * H1 ; :: thesis: the carrier of (H1 "\/" H2) = H1 * H2

then consider H being strict StableSubgroup of G such that

A1: the carrier of H = (carr H1) * (carr H2) by Th17;

now :: thesis: for a being Element of G st a in H holds

a in H1 "\/" H2

then
H is StableSubgroup of H1 "\/" H2
by Th13;a in H1 "\/" H2

set A = (carr H1) \/ (carr H2);

let a be Element of G; :: thesis: ( a in H implies a in H1 "\/" H2 )

set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;

assume a in H ; :: thesis: a in H1 "\/" H2

then a in (carr H1) * (carr H2) by A1, STRUCT_0:def 5;

then consider b, c being Element of G such that

A2: a = b * c and

A3: b in carr H1 and

A4: c in carr H2 ;

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;

then a in meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } by A5, SETFAM_1:def 1;

then a in the carrier of (the_stable_subgroup_of ((carr H1) \/ (carr H2))) by Th27;

hence a in H1 "\/" H2 by STRUCT_0:def 5; :: thesis: verum

end;let a be Element of G; :: thesis: ( a in H implies a in H1 "\/" H2 )

set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;

assume a in H ; :: thesis: a in H1 "\/" H2

then a in (carr H1) * (carr H2) by A1, STRUCT_0:def 5;

then consider b, c being Element of G such that

A2: a = b * c and

A3: b in carr H1 and

A4: c in carr H2 ;

A5: now :: thesis: for Y being set st Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } holds

a in Y

carr ((Omega). G) in { B where B is Subset of G : ex H being strict StableSubgroup of G st ( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } holds

a in Y

let Y be set ; :: thesis: ( Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } implies a in Y )

assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ; :: thesis: a in Y

then consider B being Subset of G such that

A6: Y = B and

A7: ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) ;

consider H9 being strict StableSubgroup of G such that

A8: B = the carrier of H9 and

A9: (carr H1) \/ (carr H2) c= carr H9 by A7;

c in (carr H1) \/ (carr H2) by A4, XBOOLE_0:def 3;

then A10: c in H9 by A9, STRUCT_0:def 5;

A11: H9 is Subgroup of G by Def7;

b in (carr H1) \/ (carr H2) by A3, XBOOLE_0:def 3;

then b in H9 by A9, STRUCT_0:def 5;

then b * c in H9 by A11, A10, GROUP_2:50;

hence a in Y by A2, A6, A8, STRUCT_0:def 5; :: thesis: verum

end;( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } implies a in Y )

assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ; :: thesis: a in Y

then consider B being Subset of G such that

A6: Y = B and

A7: ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) ;

consider H9 being strict StableSubgroup of G such that

A8: B = the carrier of H9 and

A9: (carr H1) \/ (carr H2) c= carr H9 by A7;

c in (carr H1) \/ (carr H2) by A4, XBOOLE_0:def 3;

then A10: c in H9 by A9, STRUCT_0:def 5;

A11: H9 is Subgroup of G by Def7;

b in (carr H1) \/ (carr H2) by A3, XBOOLE_0:def 3;

then b in H9 by A9, STRUCT_0:def 5;

then b * c in H9 by A11, A10, GROUP_2:50;

hence a in Y by A2, A6, A8, STRUCT_0:def 5; :: thesis: verum

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;

then a in meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } by A5, SETFAM_1:def 1;

then a in the carrier of (the_stable_subgroup_of ((carr H1) \/ (carr H2))) by Th27;

hence a in H1 "\/" H2 by STRUCT_0:def 5; :: thesis: verum

then H is Subgroup of H1 "\/" H2 by Def7;

then A12: the carrier of H c= the carrier of (H1 "\/" H2) by GROUP_2:def 5;

(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)

proof

then
H1 "\/" H2 is StableSubgroup of H
by A1, Def26;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H1) \/ (carr H2) or x in (carr H1) * (carr H2) )

assume A13: x in (carr H1) \/ (carr H2) ; :: thesis: x in (carr H1) * (carr H2)

then reconsider a = x as Element of G ;

end;assume A13: x in (carr H1) \/ (carr H2) ; :: thesis: x in (carr H1) * (carr H2)

then reconsider a = x as Element of G ;

now :: thesis: x in (carr H1) * (carr H2)

hence
x in (carr H1) * (carr H2)
; :: thesis: verumend;

then H1 "\/" H2 is Subgroup of H by Def7;

then the carrier of (H1 "\/" H2) c= the carrier of H by GROUP_2:def 5;

hence the carrier of (H1 "\/" H2) = H1 * H2 by A1, A12, XBOOLE_0:def 10; :: thesis: verum