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

for H being StableSubgroup of G

for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G

for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let H be StableSubgroup of G; :: thesis: for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FG be FinSequence of the carrier of G; :: thesis: for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A1: ( FG = FH & len FG = len I ) ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

defpred S_{1}[ Nat] means for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st len FG = $1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I);

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A21, A2);

hence Product (FG |^ I) = Product (FH |^ I) by A1; :: thesis: verum

for H being StableSubgroup of G

for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G

for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let H be StableSubgroup of G; :: thesis: for FG being FinSequence of the carrier of G

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FG be FinSequence of the carrier of G; :: thesis: for FH being FinSequence of the carrier of H

for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A1: ( FG = FH & len FG = len I ) ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

defpred S

for FH being FinSequence of the carrier of H

for I being FinSequence of INT st len FG = $1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I);

A2: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A21:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A3: S

thus S

proof

let FG be FinSequence of the carrier of G; :: thesis: for FH being FinSequence of the carrier of H

for I being FinSequence of INT st len FG = n + 1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st len FG = n + 1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( len FG = n + 1 & FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A4: len FG = n + 1 ; :: thesis: ( not FG = FH or not len FG = len I or Product (FG |^ I) = Product (FH |^ I) )

then consider FGn being FinSequence of the carrier of G, g being Element of G such that

A5: FG = FGn ^ <*g*> by FINSEQ_2:19;

A6: len FG = (len FGn) + (len <*g*>) by A5, FINSEQ_1:22;

then A7: n + 1 = (len FGn) + 1 by A4, FINSEQ_1:40;

assume that

A8: FG = FH and

A9: len FG = len I ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

consider FHn being FinSequence of the carrier of H, h being Element of H such that

A10: FH = FHn ^ <*h*> by A4, A8, FINSEQ_2:19;

consider In being FinSequence of INT , i being Element of INT such that

A11: I = In ^ <*i*> by A4, A9, FINSEQ_2:19;

set FG1 = <*g*>;

set I1 = <*i*>;

len I = (len In) + (len <*i*>) by A11, FINSEQ_1:22;

then A12: n + 1 = (len In) + 1 by A4, A9, FINSEQ_1:40;

A13: len FH = (len FHn) + (len <*h*>) by A10, FINSEQ_1:22;

then A14: FH . (n + 1) = (FHn ^ <*h*>) . ((len FHn) + 1) by A4, A8, A10, FINSEQ_1:40

.= h by FINSEQ_1:42 ;

A15: n + 1 = (len FHn) + 1 by A4, A8, A13, FINSEQ_1:40;

A16: FG . (n + 1) = (FGn ^ <*g*>) . ((len FGn) + 1) by A4, A5, A6, FINSEQ_1:40

.= g by FINSEQ_1:42 ;

.= len <*i*> by FINSEQ_1:40 ;

then A18: Product (FG |^ I) = Product ((FGn |^ In) ^ (<*g*> |^ <*i*>)) by A11, A5, A12, A7, GROUP_4:19

.= (Product (FGn |^ In)) * (Product (<*g*> |^ <*i*>)) by GROUP_4:5 ;

set FH1 = <*h*>;

A19: len <*h*> = 1 by FINSEQ_1:40

.= len <*i*> by FINSEQ_1:40 ;

A20: Product (<*g*> |^ <*i*>) = Product (<*g*> |^ <*(@ i)*>)

.= Product <*(g |^ i)*> by GROUP_4:22

.= h |^ i by A17, GROUP_4:9

.= Product <*(h |^ i)*> by GROUP_4:9

.= Product (<*h*> |^ <*(@ i)*>) by GROUP_4:22

.= Product (<*h*> |^ <*i*>) ;

FGn = FHn by A8, A5, A10, A16, A14, FINSEQ_1:33;

then Product (FGn |^ In) = Product (FHn |^ In) by A3, A12, A15;

then Product (FG |^ I) = (Product (FHn |^ In)) * (Product (<*h*> |^ <*i*>)) by A18, A20, Th3

.= Product ((FHn |^ In) ^ (<*h*> |^ <*i*>)) by GROUP_4:5

.= Product ((FHn ^ <*h*>) |^ (In ^ <*i*>)) by A12, A15, A19, GROUP_4:19 ;

hence Product (FG |^ I) = Product (FH |^ I) by A11, A10; :: thesis: verum

end;for I being FinSequence of INT st len FG = n + 1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st len FG = n + 1 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( len FG = n + 1 & FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A4: len FG = n + 1 ; :: thesis: ( not FG = FH or not len FG = len I or Product (FG |^ I) = Product (FH |^ I) )

then consider FGn being FinSequence of the carrier of G, g being Element of G such that

A5: FG = FGn ^ <*g*> by FINSEQ_2:19;

A6: len FG = (len FGn) + (len <*g*>) by A5, FINSEQ_1:22;

then A7: n + 1 = (len FGn) + 1 by A4, FINSEQ_1:40;

assume that

A8: FG = FH and

A9: len FG = len I ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

consider FHn being FinSequence of the carrier of H, h being Element of H such that

A10: FH = FHn ^ <*h*> by A4, A8, FINSEQ_2:19;

consider In being FinSequence of INT , i being Element of INT such that

A11: I = In ^ <*i*> by A4, A9, FINSEQ_2:19;

set FG1 = <*g*>;

set I1 = <*i*>;

len I = (len In) + (len <*i*>) by A11, FINSEQ_1:22;

then A12: n + 1 = (len In) + 1 by A4, A9, FINSEQ_1:40;

A13: len FH = (len FHn) + (len <*h*>) by A10, FINSEQ_1:22;

then A14: FH . (n + 1) = (FHn ^ <*h*>) . ((len FHn) + 1) by A4, A8, A10, FINSEQ_1:40

.= h by FINSEQ_1:42 ;

A15: n + 1 = (len FHn) + 1 by A4, A8, A13, FINSEQ_1:40;

A16: FG . (n + 1) = (FGn ^ <*g*>) . ((len FGn) + 1) by A4, A5, A6, FINSEQ_1:40

.= g by FINSEQ_1:42 ;

A17: now :: thesis: g |^ i = h |^ i

len <*g*> =
1
by FINSEQ_1:40
reconsider H9 = H as Subgroup of G by Def7;

reconsider h9 = h as Element of H9 ;

g |^ i = h9 |^ i by A8, A16, A14, GROUP_4:2;

hence g |^ i = h |^ i ; :: thesis: verum

end;reconsider h9 = h as Element of H9 ;

g |^ i = h9 |^ i by A8, A16, A14, GROUP_4:2;

hence g |^ i = h |^ i ; :: thesis: verum

.= len <*i*> by FINSEQ_1:40 ;

then A18: Product (FG |^ I) = Product ((FGn |^ In) ^ (<*g*> |^ <*i*>)) by A11, A5, A12, A7, GROUP_4:19

.= (Product (FGn |^ In)) * (Product (<*g*> |^ <*i*>)) by GROUP_4:5 ;

set FH1 = <*h*>;

A19: len <*h*> = 1 by FINSEQ_1:40

.= len <*i*> by FINSEQ_1:40 ;

A20: Product (<*g*> |^ <*i*>) = Product (<*g*> |^ <*(@ i)*>)

.= Product <*(g |^ i)*> by GROUP_4:22

.= h |^ i by A17, GROUP_4:9

.= Product <*(h |^ i)*> by GROUP_4:9

.= Product (<*h*> |^ <*(@ i)*>) by GROUP_4:22

.= Product (<*h*> |^ <*i*>) ;

FGn = FHn by A8, A5, A10, A16, A14, FINSEQ_1:33;

then Product (FGn |^ In) = Product (FHn |^ In) by A3, A12, A15;

then Product (FG |^ I) = (Product (FHn |^ In)) * (Product (<*h*> |^ <*i*>)) by A18, A20, Th3

.= Product ((FHn |^ In) ^ (<*h*> |^ <*i*>)) by GROUP_4:5

.= Product ((FHn ^ <*h*>) |^ (In ^ <*i*>)) by A12, A15, A19, GROUP_4:19 ;

hence Product (FG |^ I) = Product (FH |^ I) by A11, A10; :: thesis: verum

proof

for n being Nat holds S
let FG be FinSequence of the carrier of G; :: thesis: for FH being FinSequence of the carrier of H

for I being FinSequence of INT st len FG = 0 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st len FG = 0 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( len FG = 0 & FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A22: len FG = 0 ; :: thesis: ( not FG = FH or not len FG = len I or Product (FG |^ I) = Product (FH |^ I) )

then len (FG |^ I) = 0 by GROUP_4:def 3;

then FG |^ I = <*> the carrier of G ;

then A23: Product (FG |^ I) = 1_ G by GROUP_4:8;

assume that

A24: FG = FH and

len FG = len I ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

len (FH |^ I) = 0 by A22, A24, GROUP_4:def 3;

then FH |^ I = <*> the carrier of H ;

then Product (FH |^ I) = 1_ H by GROUP_4:8;

hence Product (FG |^ I) = Product (FH |^ I) by A23, Th4; :: thesis: verum

end;for I being FinSequence of INT st len FG = 0 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let FH be FinSequence of the carrier of H; :: thesis: for I being FinSequence of INT st len FG = 0 & FG = FH & len FG = len I holds

Product (FG |^ I) = Product (FH |^ I)

let I be FinSequence of INT ; :: thesis: ( len FG = 0 & FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )

assume A22: len FG = 0 ; :: thesis: ( not FG = FH or not len FG = len I or Product (FG |^ I) = Product (FH |^ I) )

then len (FG |^ I) = 0 by GROUP_4:def 3;

then FG |^ I = <*> the carrier of G ;

then A23: Product (FG |^ I) = 1_ G by GROUP_4:8;

assume that

A24: FG = FH and

len FG = len I ; :: thesis: Product (FG |^ I) = Product (FH |^ I)

len (FH |^ I) = 0 by A22, A24, GROUP_4:def 3;

then FH |^ I = <*> the carrier of H ;

then Product (FH |^ I) = 1_ H by GROUP_4:8;

hence Product (FG |^ I) = Product (FH |^ I) by A23, Th4; :: thesis: verum

hence Product (FG |^ I) = Product (FH |^ I) by A1; :: thesis: verum