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: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: 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 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

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;

len <*g*> = 1 by FINSEQ_1:40
.= 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;

end;

A21: 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 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 n being Nat holds S₁[n] from NAT_1:sch 2(A21, A2);
hence Product (FG |^ I) = Product (FH |^ I) by A1; :: thesis: verum