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₁[ 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);
A2: S₁[ 0 ]

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 = 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 A3: 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 4;
then FG |^ I = <*> the carrier of G ;
then A4: Product (FG |^ I) = 1_ G by GROUP_4:11;
assume ( FG = FH & len FG = len I ) ; :: thesis: Product (FG |^ I) = Product (FH |^ I)
then len (FH |^ I) = 0 by A3, GROUP_4:def 4;
then FH |^ I = <*> the carrier of H ;
then Product (FH |^ I) = 1_ H by GROUP_4:11;
hence Product (FG |^ I) = Product (FH |^ I) by A4, Th4; :: thesis: verum

end;

A5: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

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 A7: len FG = n + 1 ; :: thesis: ( not FG = FH or not len FG = len I or Product (FG |^ I) = Product (FH |^ I) )
assume A8: ( FG = FH & len FG = len I ) ; :: thesis: Product (FG |^ I) = Product (FH |^ I)
then consider In being FinSequence of INT , i being Element of INT such that
A9: I = In ^ <*i*> by A7, FINSEQ_2:22;
consider FGn being FinSequence of the carrier of G, g being Element of G such that
A10: FG = FGn ^ <*g*> by A7, FINSEQ_2:22;
consider FHn being FinSequence of the carrier of H, h being Element of H such that
A11: FH = FHn ^ <*h*> by A7, A8, FINSEQ_2:22;
set I1 = <*i*>;
set FG1 = <*g*>;
set FH1 = <*h*>;
len I = (len In) + (len <*i*>) by A9, FINSEQ_1:35;
then A12: n + 1 = (len In) + 1 by A7, A8, FINSEQ_1:57;
A13: len FG = (len FGn) + (len <*g*>) by A10, FINSEQ_1:35;
then A14: n + 1 = (len FGn) + 1 by A7, FINSEQ_1:57;
A15: len FH = (len FHn) + (len <*h*>) by A11, FINSEQ_1:35;
then A16: n + 1 = (len FHn) + 1 by A7, A8, FINSEQ_1:57;
A17: FG . (n + 1) = (FGn ^ <*g*>) . ((len FGn) + 1) by A7, A10, A13, FINSEQ_1:57
.= g by FINSEQ_1:59 ;
A18: FH . (n + 1) = (FHn ^ <*h*>) . ((len FHn) + 1) by A7, A8, A11, A15, FINSEQ_1:57
.= h by FINSEQ_1:59 ;
then FGn = FHn by A8, A10, A11, A17, FINSEQ_1:46;
then A19: Product (FGn |^ In) = Product (FHn |^ In) by A6, A12, A16;
A20: len <*g*> = 1 by FINSEQ_1:57
.= len <*i*> by FINSEQ_1:57 ;
A21: len <*h*> = 1 by FINSEQ_1:57
.= len <*i*> by FINSEQ_1:57 ;
A22: Product (FG |^ I) = Product ((FGn |^ In) ^ (<*g*> |^ <*i*>)) by A9, A10, A12, A14, A20, GROUP_4:25
.= (Product (FGn |^ In)) * (Product (<*g*> |^ <*i*>)) by GROUP_4:8 ;

A23: now

reconsider H' = H as Subgroup of G by Def7;
reconsider h' = h as Element of H' ;
g |^ i = h' |^ i by A8, A17, A18, GROUP_4:4;
hence g |^ i = h |^ i ; :: thesis: verum

end;

Product (<*g*> |^ <*i*>) = Product (<*g*> |^ <*(@ i)*>)
.= Product <*(g |^ i)*> by GROUP_4:28
.= h |^ i by A23, GROUP_4:12
.= Product <*(h |^ i)*> by GROUP_4:12
.= Product (<*h*> |^ <*(@ i)*>) by GROUP_4:28
.= Product (<*h*> |^ <*i*>) ;
then Product (FG |^ I) = (Product (FHn |^ In)) * (Product (<*h*> |^ <*i*>)) by A19, A22, Th3
.= Product ((FHn |^ In) ^ (<*h*> |^ <*i*>)) by GROUP_4:8
.= Product ((FHn ^ <*h*>) |^ (In ^ <*i*>)) by A12, A16, A21, GROUP_4:25 ;
hence Product (FG |^ I) = Product (FH |^ I) by A9, A11; :: thesis: verum

end;

end;

A24: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A5);
thus Product (FG |^ I) = Product (FH |^ I) by A1, A24; :: thesis: verum