let G be Group; for H being Subgroup of G
for f being FinSequence of G
for g being FinSequence of H st f = g holds
Product f = Product g
let H be Subgroup of G; for f being FinSequence of G
for g being FinSequence of H st f = g holds
Product f = Product g
defpred S1[ Nat] means for f being FinSequence of G
for g being FinSequence of H st $1 = len f & f = g holds
Product f = Product g;
A1:
S1[ 0 ]
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let f be
FinSequence of
G;
for g being FinSequence of H st k + 1 = len f & f = g holds
Product f = Product glet g be
FinSequence of
H;
( k + 1 = len f & f = g implies Product f = Product g )
assume A6:
(
k + 1
= len f &
f = g )
;
Product f = Product g
A7:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then
k + 1
in dom f
by A6, FINSEQ_1:def 3;
then
f . (k + 1) in rng f
by FUNCT_1:3;
then reconsider af =
f . (k + 1) as
Element of
G ;
k + 1
in dom g
by A7, A6, FINSEQ_1:def 3;
then
g . (k + 1) in rng g
by FUNCT_1:3;
then reconsider ag =
g . (k + 1) as
Element of
H ;
reconsider f1 =
f | k as
FinSequence of
G ;
reconsider g1 =
g | k as
FinSequence of
H ;
A8:
f = f1 ^ <*af*>
by A6, RFINSEQ:7;
A9:
g = g1 ^ <*ag*>
by A6, RFINSEQ:7;
A10:
Product f = (Product f1) * af
by GROUP_4:6, A8;
A11:
Product g = (Product g1) * ag
by GROUP_4:6, A9;
len f1 = k
by FINSEQ_1:59, A6, NAT_1:11;
then
Product f1 = Product g1
by A6, A5;
hence
Product f = Product g
by A10, A11, GROUP_2:43, A6;
verum
end;
A12:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A4);
let f be FinSequence of G; for g being FinSequence of H st f = g holds
Product f = Product g
let g be FinSequence of H; ( f = g implies Product f = Product g )
assume A13:
f = g
; Product f = Product g
len f is Nat
;
hence
Product f = Product g
by A13, A12; verum