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) + () 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 ; :: thesis: 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 :: thesis: 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; :: 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 A9: 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 ) )

then A10: 0 + 1 < k + 1 by XREAL_1:6;
assume A11: 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 ;
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; :: 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 )
1 <= k by ;
then k in Seg (len F) by A11;
hence f = PF . k by ; :: thesis: ( g = A . (F . (k + 1)) & PF . (k + 1) = f * g )
k + 1 <= len F by ;
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 ; :: thesis: PF . (k + 1) = f * g
thus PF . (k + 1) = f * g by ; :: thesis: verum
end;
A16: len F < len (F ^ <*o*>) by ;
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 ;
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 ;
Seg (len F) c= Seg (len PF1) by ;
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 ;
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 ;
PF . 1 = A . ((F ^ <*o*>) . 1) by
.= A . (F . 1) by ;
then IT = Product (F,A) by A6, A21, A8, Def3;
hence Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A)) by ; :: thesis: verum
end;
suppose A22: len F = 0 ; :: thesis: Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A))
then F = <*> O ;
hence Product ((F ^ <*o*>),A) = Product (<*o*>,A) by FINSEQ_1:34
.= (id E) * (Product (<*o*>,A)) by FUNCT_2:17
.= (Product (F,A)) * (Product (<*o*>,A)) by ;
:: thesis: verum
end;
end;