let O be non empty set ; 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 ; 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; 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; 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; 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:22
.=
(len F) + 1
by FINSEQ_1:39
;
consider PF1 being FinSequence of Funcs (E,E) such that
A2:
Product ((F ^ <*o*>),A) = PF1 . (len (F ^ <*o*>))
and
A3:
len PF1 = len (F ^ <*o*>)
and
A4:
PF1 . 1 = A . ((F ^ <*o*>) . 1)
and
A5:
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 A6:
len F <> 0
;
Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A))reconsider PF =
PF1 | (Seg (len F)) as
FinSequence of
Funcs (
E,
E)
by FINSEQ_1:18;
set IT =
PF . (len F);
A7:
Product (
<*o*>,
A) =
A . o
by Lm25
.=
A . ((F ^ <*o*>) . ((len F) + 1))
by FINSEQ_1:42
;
A8:
now for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )let k be
Nat;
( 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 A9:
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 ) )then A10:
0 + 1
< k + 1
by XREAL_1:6;
assume A11:
k < len F
;
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 A12:
f = PF1 . k
and A13:
g = A . ((F ^ <*o*>) . (k + 1))
and A14:
PF1 . (k + 1) = f * g
by A5, A9;
take f =
f;
ex g being Function of E,E st
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )take g =
g;
( f = PF . k & g = A . (F . (k + 1)) & PF . (k + 1) = f * g )
1
<= k
by A10, NAT_1:13;
then
k in Seg (len F)
by A11;
hence
f = PF . k
by A12, FUNCT_1:49;
( g = A . (F . (k + 1)) & PF . (k + 1) = f * g )
k + 1
<= len F
by A11, NAT_1:13;
then A15:
k + 1
in Seg (len F)
by A10;
then
k + 1
in dom F
by FINSEQ_1:def 3;
hence
g = A . (F . (k + 1))
by A13, FINSEQ_1:def 7;
PF . (k + 1) = f * gthus
PF . (k + 1) = f * g
by A14, A15, FUNCT_1:49;
verum end; A16:
len F < len (F ^ <*o*>)
by A1, NAT_1:13;
then A17:
ex
f,
g being
Function of
E,
E st
(
f = PF1 . (len F) &
g = A . ((F ^ <*o*>) . ((len F) + 1)) &
PF1 . ((len F) + 1) = f * g )
by A5, A6;
0 + 1
< (len F) + 1
by A6, XREAL_1:6;
then
1
<= len F
by NAT_1:13;
then A18:
1
in Seg (len F)
;
then A19:
1
in dom F
by FINSEQ_1:def 3;
A20:
len F in Seg (len F)
by A6, FINSEQ_1:3;
Seg (len F) c= Seg (len PF1)
by A3, A16, FINSEQ_1:5;
then
len F in Seg (len PF1)
by A20;
then
len F in dom PF1
by FINSEQ_1:def 3;
then
len F in (dom PF1) /\ (Seg (len F))
by A20, XBOOLE_0:def 4;
then
len F in dom PF
by RELAT_1:61;
then
PF . (len F) in rng PF
by FUNCT_1:3;
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:2;
A21:
len PF = len F
by A3, A16, FINSEQ_1:17;
PF . 1 =
A . ((F ^ <*o*>) . 1)
by A4, A18, FUNCT_1:49
.=
A . (F . 1)
by A19, FINSEQ_1:def 7
;
then
IT = Product (
F,
A)
by A6, A21, A8, Def3;
hence
Product (
(F ^ <*o*>),
A)
= (Product (F,A)) * (Product (<*o*>,A))
by A1, A2, A6, A17, A7, FINSEQ_1:3, FUNCT_1:49;
verum end;