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 S1[ 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 S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
thus S1[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) + () by ;
then A7: n + 1 = (len FGn) + 1 by ;
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 ;
consider In being FinSequence of INT , i being Element of INT such that
A11: I = In ^ <*i*> by ;
set FG1 = <*g*>;
set I1 = <*i*>;
len I = (len In) + () by ;
then A12: n + 1 = (len In) + 1 by ;
A13: len FH = (len FHn) + () by ;
then A14: FH . (n + 1) = (FHn ^ <*h*>) . ((len FHn) + 1) by
.= h by FINSEQ_1:42 ;
A15: n + 1 = (len FHn) + 1 by ;
A16: FG . (n + 1) = (FGn ^ <*g*>) . ((len FGn) + 1) by
.= 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 ;
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) ^ ()) by
.= (Product (FGn |^ In)) * (Product ()) by GROUP_4:5 ;
set FH1 = <*h*>;
A19: len <*h*> = 1 by FINSEQ_1:40
.= len <*i*> by FINSEQ_1:40 ;
A20: Product () = Product (<*g*> |^ <*(@ i)*>)
.= Product <*(g |^ i)*> by GROUP_4:22
.= h |^ i by
.= Product <*(h |^ i)*> by GROUP_4:9
.= Product (<*h*> |^ <*(@ i)*>) by GROUP_4:22
.= Product () ;
FGn = FHn by ;
then Product (FGn |^ In) = Product (FHn |^ In) by A3, A12, A15;
then Product (FG |^ I) = (Product (FHn |^ In)) * (Product ()) by
.= Product ((FHn |^ In) ^ ()) by GROUP_4:5
.= Product ((FHn ^ <*h*>) |^ (In ^ <*i*>)) by ;
hence Product (FG |^ I) = Product (FH |^ I) by ; :: thesis: verum
end;
end;
A21: S1[ 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 ;
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 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A21, A2);
hence Product (FG |^ I) = Product (FH |^ I) by A1; :: thesis: verum