let O be set ; 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; 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; 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; 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; 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 ; ( FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )
assume A1:
( FG = FH & len FG = len I )
; 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 for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A3:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let FG be
FinSequence of the
carrier of
G;
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;
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 ;
( len FG = n + 1 & FG = FH & len FG = len I implies Product (FG |^ I) = Product (FH |^ I) )
assume A4:
len FG = n + 1
;
( 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
;
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 <*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;
verum
end; end;
A21:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A21, A2);
hence
Product (FG |^ I) = Product (FH |^ I)
by A1; verum