let G be Group; :: thesis:
let H1, H2 be Subgroup of G; :: thesis:
set H = gr ((carr H1) * (carr H2));

let a be Element of G; :: thesis:
assume a in gr ((carr H1) * (carr H2)) ; :: thesis:
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A1: len F = len I and
A2: rng F c= (carr H1) * (carr H2) and
A3: a = Product (F |^ I) by Th28;
rng (F |^ I) c= carr (H1 "\/" H2)

set f = F |^ I;
let x be object ; :: according to TARSKI:def 3 :: thesis:
A4: rng I c= INT by FINSEQ_1:def 4;
assume x in rng (F |^ I) ; :: thesis:
then consider y being object such that
A5: y in dom (F |^ I) and
A6: (F |^ I) . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A5;
A7: len (F |^ I) = len F by Def3;
then A8: y in dom I by A1, A5, FINSEQ_3:29;
then A9: I /. y = I . y by PARTFUN1:def 6;
I . y in rng I by A8, FUNCT_1:def 3;
then reconsider i = I . y as Integer by A4;
A10: @ (I /. y) = I /. y ;
y in dom F by A5, A7, FINSEQ_3:29;
then ( F /. y = F . y & F . y in rng F ) by FUNCT_1:def 3, PARTFUN1:def 6;
then consider b, c being Element of G such that
A11: F /. y = b * c and
A12: b in carr H1 and
A13: c in carr H2 by A2, GROUP_2:8;
y in dom F by A5, A7, FINSEQ_3:29;
then A14: x = (F /. y) |^ i by A6, A9, A10, Def3;

now :: thesis:

per cases ;

suppose i >= 0 ; :: thesis:

then reconsider n = i as Element of NAT by INT_1:3;
defpred S₁[ Nat, object ] means ( ( $1 mod 2 = 1 implies $2 = b ) & ( $1 mod 2 = 0 implies $2 = c ) );
A15: for k being Nat st k in Seg (2 * n) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (2 * n) ; :: thesis:

now :: thesis:

per cases by NAT_D:12;

suppose A16: k mod 2 = 1 ; :: thesis:

reconsider x = b as set ;
take x = x; :: thesis:
thus ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) ) by A16; :: thesis:

end;

suppose A17: k mod 2 = 0 ; :: thesis:

reconsider x = c as set ;
take x = x; :: thesis:
thus ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) ) by A17; :: thesis:

end;

hence ex x being object st S₁[k,x] ; :: thesis:

end;

consider p being FinSequence such that
A18: dom p = Seg (2 * n) and
A19: for k being Nat st k in Seg (2 * n) holds
S₁[k,p . k] from FINSEQ_1:sch 1(A15);
A20: len p = 2 * n by A18, FINSEQ_1:def 3;
A21: rng p c= {b,c}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being object such that
A22: y in dom p and
A23: p . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A22;

now :: thesis:

per cases by NAT_D:12;

suppose y mod 2 = 0 ; :: thesis:

then x = c by A18, A19, A22, A23;
hence x in {b,c} by TARSKI:def 2; :: thesis:

end;

suppose y mod 2 = 1 ; :: thesis:

then x = b by A18, A19, A22, A23;
hence x in {b,c} by TARSKI:def 2; :: thesis:

end;

hence x in {b,c} ; :: thesis:

end;

then rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def 4;
A24: ( (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) & carr (gr ((carr H1) \/ (carr H2))) = the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4;
defpred S₂[ Nat] means ( $1 <= 2 * n & $1 mod 2 = 0 implies for F1 being FinSequence of the carrier of G st F1 = p | (Seg $1) holds
Product F1 = (F /. y) |^ ($1 div 2) );
A25: for k being Nat st ( for l being Nat st l < k holds
S₂[l] ) holds
S₂[k]

proof

let k be Nat; :: thesis:
assume A26: for l being Nat st l < k holds
S₂[l] ; :: thesis:
assume that
A27: k <= 2 * n and
A28: k mod 2 = 0 ; :: thesis:
let F1 be FinSequence of the carrier of G; :: thesis:
assume A29: F1 = p | (Seg k) ; :: thesis:

now :: thesis:

per cases ;

suppose A30: k = 0 ; :: thesis:

2 * 0 = 0 ;
then A31: 0 div 2 = 0 by NAT_D:18;
F1 = <*> the carrier of G by A29, A30;
then Product F1 = 1_ G by Th8;
hence Product F1 = (F /. y) |^ (k div 2) by A30, A31, GROUP_1:25; :: thesis:

end;

suppose A32: k <> 0 ; :: thesis:

A33: k <> 1 by A28, NAT_D:14;
k >= 1 by A32, NAT_1:14;
then k > 1 by A33, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | (Seg m) as FinSequence of the carrier of G by FINSEQ_1:18;
1 * 2 = 2 ;
then A34: m mod 2 = 0 by A28, NAT_D:15;
A35: m + 2 = k ;
then A36: m <= 2 * n by A27, NAT_1:16, XXREAL_0:2;
then ex o being Nat st 2 * n = m + o by NAT_1:10;
then A37: len q = m by A20, FINSEQ_3:53;
A38: ex j being Nat st 2 * n = k + j by A27, NAT_1:10;
then A39: len F1 = k by A20, A29, FINSEQ_3:53;

A40: now :: thesis:

let l be Nat; :: thesis:
assume A41: l in dom q ; :: thesis:
then l <= len q by FINSEQ_3:25;
then A42: l <= len F1 by A35, A39, A37, NAT_1:16, XXREAL_0:2;
1 <= l by A41, FINSEQ_3:25;
then l in dom F1 by A42, FINSEQ_3:25;
then F1 . l = p . l by A29, FUNCT_1:47;
hence F1 . l = q . l by A41, FUNCT_1:47; :: thesis:

end;

A43: m < k by A35, NAT_1:16;
then A44: Product q = (F /. y) |^ (m div 2) by A26, A36, A34;

A45: now :: thesis:

let l be Nat; :: thesis:
assume l in dom <*b,c*> ; :: thesis:
then A46: l in {1,2} by FINSEQ_1:2, FINSEQ_1:89;

now :: thesis:

per cases by A46, TARSKI:def 2;

suppose A47: l = 1 ; :: thesis:

then A48: <*b,c*> . l = b by FINSEQ_1:44;
A49: ( (m + 1) mod 2 = 1 & dom F1 c= dom p ) by A29, A34, NAT_D:16, RELAT_1:60;
( m + 1 <= k & 1 <= m + 1 ) by A43, NAT_1:12, NAT_1:13;
then A50: m + 1 in dom F1 by A39, FINSEQ_3:25;
then F1 . ((len q) + l) = p . (m + 1) by A29, A37, A47, FUNCT_1:47;
hence F1 . ((len q) + l) = <*b,c*> . l by A18, A19, A48, A50, A49; :: thesis:

end;

suppose A51: l = 2 ; :: thesis:

then A52: <*b,c*> . l = c by FINSEQ_1:44;
A53: dom F1 c= dom p by A29, RELAT_1:60;
1 <= m + (1 + 1) by NAT_1:12;
then A54: m + 2 in dom F1 by A39, FINSEQ_3:25;
then F1 . ((len q) + l) = p . (m + 2) by A29, A37, A51, FUNCT_1:47;
hence F1 . ((len q) + l) = <*b,c*> . l by A18, A19, A28, A52, A54, A53; :: thesis:

end;

hence F1 . ((len q) + l) = <*b,c*> . l ; :: thesis:

end;

A55: (m div (2 * 1)) + 1 = (m div 2) + (2 div 2) by NAT_D:18
.= k div 2 by A35, A34, NAT_D:19 ;
len F1 = m + 2 by A20, A29, A38, FINSEQ_3:53
.= (len q) + (len <*b,c*>) by A37, FINSEQ_1:44 ;
then F1 = q ^ <*b,c*> by A40, A45, FINSEQ_3:38;
then Product F1 = (Product q) * (Product <*b,c*>) by FINSOP_1:5
.= (Product q) * (F /. y) by A11, FINSOP_1:12
.= (F /. y) |^ ((m div 2) + 1) by A44, GROUP_1:34 ;
hence Product F1 = (F /. y) |^ (k div 2) by A55; :: thesis:

end;

hence Product F1 = (F /. y) |^ (k div 2) ; :: thesis:

end;

A56: for k being Nat holds S₂[k] from NAT_1:sch 4(A25);
( b in (carr H1) \/ (carr H2) & c in (carr H1) \/ (carr H2) ) by A12, A13, XBOOLE_0:def 3;
then {b,c} c= (carr H1) \/ (carr H2) by ZFMISC_1:32;
then A57: rng p c= (carr H1) \/ (carr H2) by A21;
len p = 2 * n by A18, FINSEQ_1:def 3;
then A58: p = p | (Seg (2 * n)) by FINSEQ_3:49;
( (2 * n) mod 2 = 0 & (2 * n) div 2 = n ) by NAT_D:13, NAT_D:18;
then x = Product p by A14, A56, A58;
then x in gr ((carr H1) \/ (carr H2)) by A57, A24, Th18, XBOOLE_1:1;
hence x in carr (H1 "\/" H2) by STRUCT_0:def 5; :: thesis:

end;

suppose A59: i < 0 ; :: thesis:

defpred S₁[ Nat, object ] means ( ( $1 mod 2 = 1 implies $2 = c " ) & ( $1 mod 2 = 0 implies $2 = b " ) );
set n = |.i.|;
A60: ( (2 * |.i.|) mod 2 = 0 & (2 * |.i.|) div 2 = |.i.| ) by NAT_D:13, NAT_D:18;
A61: for k being Nat st k in Seg (2 * |.i.|) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (2 * |.i.|) ; :: thesis:

now :: thesis:

per cases by NAT_D:12;

suppose A62: k mod 2 = 1 ; :: thesis:

reconsider x = c " as set ;
take x = x; :: thesis:
thus ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) ) by A62; :: thesis:

end;

suppose A63: k mod 2 = 0 ; :: thesis:

reconsider x = b " as set ;
take x = x; :: thesis:
thus ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) ) by A63; :: thesis:

end;

hence ex x being object st S₁[k,x] ; :: thesis:

end;

consider p being FinSequence such that
A64: dom p = Seg (2 * |.i.|) and
A65: for k being Nat st k in Seg (2 * |.i.|) holds
S₁[k,p . k] from FINSEQ_1:sch 1(A61);
A66: len p = 2 * |.i.| by A64, FINSEQ_1:def 3;
A67: rng p c= {(b "),(c ")}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being object such that
A68: y in dom p and
A69: p . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A68;

now :: thesis:

per cases by NAT_D:12;

suppose y mod 2 = 0 ; :: thesis:

then x = b " by A64, A65, A68, A69;
hence x in {(b "),(c ")} by TARSKI:def 2; :: thesis:

end;

suppose y mod 2 = 1 ; :: thesis:

then x = c " by A64, A65, A68, A69;
hence x in {(b "),(c ")} by TARSKI:def 2; :: thesis:

end;

hence x in {(b "),(c ")} ; :: thesis:

end;

then rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def 4;
A70: ( (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) & carr (gr ((carr H1) \/ (carr H2))) = the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4;
defpred S₂[ Nat] means ( $1 <= 2 * |.i.| & $1 mod 2 = 0 implies for F1 being FinSequence of the carrier of G st F1 = p | (Seg $1) holds
Product F1 = ((F /. y) |^ ($1 div 2)) " );
A71: for k being Nat st ( for l being Nat st l < k holds
S₂[l] ) holds
S₂[k]

proof

let k be Nat; :: thesis:
assume A72: for l being Nat st l < k holds
S₂[l] ; :: thesis:
assume that
A73: k <= 2 * |.i.| and
A74: k mod 2 = 0 ; :: thesis:
let F1 be FinSequence of the carrier of G; :: thesis:
assume A75: F1 = p | (Seg k) ; :: thesis:

now :: thesis:

per cases ;

suppose A76: k = 0 ; :: thesis:

2 * 0 = 0 ;
then 0 div 2 = 0 by NAT_D:18;
then A77: (F /. y) |^ (k div 2) = 1_ G by A76, GROUP_1:25;
F1 = <*> the carrier of G by A75, A76;
then Product F1 = 1_ G by Th8;
hence Product F1 = ((F /. y) |^ (k div 2)) " by A77, GROUP_1:8; :: thesis:

end;

suppose A78: k <> 0 ; :: thesis:

A79: k <> 1 by A74, NAT_D:14;
k >= 1 by A78, NAT_1:14;
then k > 1 by A79, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | (Seg m) as FinSequence of the carrier of G by FINSEQ_1:18;
1 * 2 = 2 ;
then A80: m mod 2 = 0 by A74, NAT_D:15;
A81: m + 2 = k ;
then A82: m <= 2 * |.i.| by A73, NAT_1:16, XXREAL_0:2;
then ex o being Nat st 2 * |.i.| = m + o by NAT_1:10;
then A83: len q = m by A66, FINSEQ_3:53;
A84: ex j being Nat st 2 * |.i.| = k + j by A73, NAT_1:10;
then A85: len F1 = k by A66, A75, FINSEQ_3:53;

A86: now :: thesis:

let l be Nat; :: thesis:
assume A87: l in dom q ; :: thesis:
then l <= len q by FINSEQ_3:25;
then A88: l <= len F1 by A81, A85, A83, NAT_1:16, XXREAL_0:2;
1 <= l by A87, FINSEQ_3:25;
then l in dom F1 by A88, FINSEQ_3:25;
then F1 . l = p . l by A75, FUNCT_1:47;
hence F1 . l = q . l by A87, FUNCT_1:47; :: thesis:

end;

A89: m < k by A81, NAT_1:16;
then A90: Product q = ((F /. y) |^ (m div 2)) " by A72, A82, A80;

A91: now :: thesis:

let l be Nat; :: thesis:
assume l in dom <*(c "),(b ")*> ; :: thesis:
then A92: l in {1,2} by FINSEQ_1:2, FINSEQ_1:89;

now :: thesis:

per cases by A92, TARSKI:def 2;

suppose A93: l = 1 ; :: thesis:

then A94: <*(c "),(b ")*> . l = c " by FINSEQ_1:44;
A95: ( (m + 1) mod 2 = 1 & dom F1 c= dom p ) by A75, A80, NAT_D:16, RELAT_1:60;
( m + 1 <= k & 1 <= m + 1 ) by A89, NAT_1:12, NAT_1:13;
then A96: m + 1 in dom F1 by A85, FINSEQ_3:25;
then F1 . ((len q) + l) = p . (m + 1) by A75, A83, A93, FUNCT_1:47;
hence F1 . ((len q) + l) = <*(c "),(b ")*> . l by A64, A65, A94, A96, A95; :: thesis:

end;

suppose A97: l = 2 ; :: thesis:

then A98: <*(c "),(b ")*> . l = b " by FINSEQ_1:44;
A99: dom F1 c= dom p by A75, RELAT_1:60;
1 <= m + (1 + 1) by NAT_1:12;
then A100: m + 2 in dom F1 by A85, FINSEQ_3:25;
then F1 . ((len q) + l) = p . (m + 2) by A75, A83, A97, FUNCT_1:47;
hence F1 . ((len q) + l) = <*(c "),(b ")*> . l by A64, A65, A74, A98, A100, A99; :: thesis:

end;

hence F1 . ((len q) + l) = <*(c "),(b ")*> . l ; :: thesis:

end;

A101: (m div (2 * 1)) + 1 = (m div 2) + (2 div 2) by NAT_D:18
.= k div 2 by A81, A80, NAT_D:19 ;
len F1 = m + 2 by A66, A75, A84, FINSEQ_3:53
.= (len q) + (len <*(c "),(b ")*>) by A83, FINSEQ_1:44 ;
then F1 = q ^ <*(c "),(b ")*> by A86, A91, FINSEQ_3:38;
then Product F1 = (Product q) * (Product <*(c "),(b ")*>) by FINSOP_1:5
.= (Product q) * ((c ") * (b ")) by FINSOP_1:12
.= (Product q) * ((F /. y) ") by A11, GROUP_1:17
.= ((F /. y) * ((F /. y) |^ (m div 2))) " by A90, GROUP_1:17
.= ((F /. y) |^ ((m div 2) + 1)) " by GROUP_1:34 ;
hence Product F1 = ((F /. y) |^ (k div 2)) " by A101; :: thesis:

end;

hence Product F1 = ((F /. y) |^ (k div 2)) " ; :: thesis:

end;

A102: for k being Nat holds S₂[k] from NAT_1:sch 4(A71);
c " in carr H2 by A13, GROUP_2:75;
then A103: c " in (carr H1) \/ (carr H2) by XBOOLE_0:def 3;
len p = 2 * |.i.| by A64, FINSEQ_1:def 3;
then A104: p = p | (Seg (2 * |.i.|)) by FINSEQ_3:49;
b " in carr H1 by A12, GROUP_2:75;
then b " in (carr H1) \/ (carr H2) by XBOOLE_0:def 3;
then {(b "),(c ")} c= (carr H1) \/ (carr H2) by A103, ZFMISC_1:32;
then A105: rng p c= (carr H1) \/ (carr H2) by A67;
x = ((F /. y) |^ |.i.|) " by A14, A59, GROUP_1:30;
then x = Product p by A102, A60, A104;
then x in gr ((carr H1) \/ (carr H2)) by A105, A70, Th18, XBOOLE_1:1;
hence x in carr (H1 "\/" H2) by STRUCT_0:def 5; :: thesis:

end;

hence x in carr (H1 "\/" H2) ; :: thesis:

end;

hence a in H1 "\/" H2 by A3, Th18; :: thesis:

end;

then A106: gr ((carr H1) * (carr H2)) is Subgroup of H1 "\/" H2 by GROUP_2:58;
(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A107: x in (carr H1) \/ (carr H2) ; :: thesis:
then reconsider a = x as Element of G ;

now :: thesis:

per cases by A107, XBOOLE_0:def 3;

suppose A108: x in carr H1 ; :: thesis:

1_ G in H2 by GROUP_2:46;
then A109: 1_ G in carr H2 by STRUCT_0:def 5;
a * (1_ G) = a by GROUP_1:def 4;
hence x in (carr H1) * (carr H2) by A108, A109; :: thesis:

end;

suppose A110: x in carr H2 ; :: thesis:

1_ G in H1 by GROUP_2:46;
then A111: 1_ G in carr H1 by STRUCT_0:def 5;
(1_ G) * a = a by GROUP_1:def 4;
hence x in (carr H1) * (carr H2) by A110, A111; :: thesis:

end;

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

end;

then H1 "\/" H2 is Subgroup of gr ((carr H1) * (carr H2)) by Th32;
hence gr (H1 * H2) = H1 "\/" H2 by A106, GROUP_2:55; :: thesis: