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: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;

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: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 )
;

end;

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 ;

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; :: thesis: verum

end;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 )

A16:
len F < len (F ^ <*o*>)
by A1, NAT_1:13;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 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; :: 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 A10, NAT_1:13;

then k in Seg (len F) by A11;

hence f = PF . k by A12, FUNCT_1:49; :: thesis: ( 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; :: thesis: PF . (k + 1) = f * g

thus PF . (k + 1) = f * g by A14, A15, FUNCT_1:49; :: thesis: verum

end;( 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 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; :: 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 A10, NAT_1:13;

then k in Seg (len F) by A11;

hence f = PF . k by A12, FUNCT_1:49; :: thesis: ( 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; :: thesis: PF . (k + 1) = f * g

thus PF . (k + 1) = f * g by A14, A15, FUNCT_1:49; :: thesis: verum

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; :: thesis: verum

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 A22, Def3 ;

:: thesis: verum

end;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 A22, Def3 ;

:: thesis: verum