let O be non empty set ; :: thesis: for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
let E be set ; :: thesis: for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
let o be Element of O; :: thesis: for F being FinSequence of O
for A being Action of O,E holds Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
let F be FinSequence of O; :: thesis: for A being Action of O,E holds Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
let A be Action of O,E; :: thesis: Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
set F1 = F ^ <*o*>;
A1: len (F ^ <*o*>) =
(len F) + (len <*o*>)
by FINSEQ_1:35
.=
(len F) + 1
by FINSEQ_1:56
;
consider PF1 being FinSequence of Funcs E,E such that
A2:
( Product (F ^ <*o*>),A = PF1 . (len (F ^ <*o*>)) & len PF1 = len (F ^ <*o*>) & PF1 . 1 = A . ((F ^ <*o*>) . 1) & ( for k being Nat st k <> 0 & k < len (F ^ <*o*>) holds
ex f, g being Function of E,E st
( f = PF1 . k & g = A . ((F ^ <*o*>) . (k + 1)) & PF1 . (k + 1) = f * g ) ) )
by Def3;
per cases
( len F <> 0 or len F = 0 )
;
suppose A3:
len F <> 0
;
:: thesis: Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)A4:
len F < len (F ^ <*o*>)
by A1, NAT_1:13;
then consider f,
g being
Function of
E,
E such that A5:
(
f = PF1 . (len F) &
g = A . ((F ^ <*o*>) . ((len F) + 1)) &
PF1 . ((len F) + 1) = f * g )
by A2, A3;
A6:
Product <*o*>,
A =
A . o
by Lm26
.=
A . ((F ^ <*o*>) . ((len F) + 1))
by FINSEQ_1:59
;
reconsider PF =
PF1 | (Seg (len F)) as
FinSequence of
Funcs E,
E by FINSEQ_1:23;
set IT =
PF . (len F);
A7:
len F in Seg (len F)
by A3, FINSEQ_1:5;
Seg (len F) c= Seg (len PF1)
by A2, A4, FINSEQ_1:7;
then
len F in Seg (len PF1)
by A7;
then
len F in dom PF1
by FINSEQ_1:def 3;
then
len F in (dom PF1) /\ (Seg (len F))
by A7, XBOOLE_0:def 4;
then
len F in dom PF
by RELAT_1:90;
then
PF . (len F) in rng PF
by FUNCT_1:12;
then
ex
f being
Function st
(
PF . (len F) = f &
dom f = E &
rng f c= E )
by FUNCT_2:def 2;
then reconsider IT =
PF . (len F) as
Function of
E,
E by FUNCT_2:4;
A8:
len PF = len F
by A2, A4, FINSEQ_1:21;
0 < len F
by A3;
then
0 + 1
< (len F) + 1
by XREAL_1:8;
then
1
<= len F
by NAT_1:13;
then A9:
1
in Seg (len F)
;
then A10:
1
in dom F
by FINSEQ_1:def 3;
A11:
PF . 1 =
A . ((F ^ <*o*>) . 1)
by A2, A9, FUNCT_1:72
.=
A . (F . 1)
by A10, FINSEQ_1:def 7
;
now let k be
Nat;
:: thesis: ( k <> 0 & k < len F implies ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g ) )assume A12:
k <> 0
;
:: thesis: ( k < len F implies ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g ) )assume A13:
k < len F
;
:: thesis: ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )then
k < len (F ^ <*o*>)
by A1, NAT_1:13;
then consider f,
g being
Function of
E,
E such that A14:
(
f = PF1 . k &
g = A . ((F ^ <*o*>) . (k + 1)) &
PF1 . (k + 1) = f * g )
by A2, A12;
take f =
f;
:: thesis: ex g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )take g =
g;
:: thesis: ( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )
0 < k
by A12;
then A15:
0 + 1
< k + 1
by XREAL_1:8;
then
1
<= k
by NAT_1:13;
then A16:
k in Seg (len F)
by A13, FINSEQ_1:3;
k + 1
<= len F
by A13, NAT_1:13;
then A17:
k + 1
in Seg (len F)
by A15;
then A18:
k + 1
in dom F
by FINSEQ_1:def 3;
thus
f = PF . k
by A14, A16, FUNCT_1:72;
:: thesis: ( g = A . (F . (k + 1)) & PF . (k + 1) = f * g )thus
g = A . (F . (k + 1))
by A14, A18, FINSEQ_1:def 7;
:: thesis: PF . (k + 1) = f * gthus
PF . (k + 1) = f * g
by A14, A17, FUNCT_1:72;
:: thesis: verum end; then A19:
IT = Product F,
A
by A3, A8, A11, Def3;
len F in Seg (len F)
by A3, FINSEQ_1:5;
hence
Product (F ^ <*o*>),
A = (Product F,A) * (Product <*o*>,A)
by A1, A2, A5, A6, A19, FUNCT_1:72;
:: thesis: verum end;