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 ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,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 ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let o be Element of O; :: thesis: for F being FinSequence of O

for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let F be FinSequence of O; :: thesis: for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let A be Action of O,E; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

defpred S_{1}[ Nat] means for F being FinSequence of O st len F = $1 holds

Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A));

reconsider k = len F as Element of NAT ;

A1: k = len F ;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A7, A2);

hence Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) by A1; :: thesis: verum

for o being Element of O

for F being FinSequence of O

for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,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 ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let o be Element of O; :: thesis: for F being FinSequence of O

for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let F be FinSequence of O; :: thesis: for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let A be Action of O,E; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

defpred S

Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A));

reconsider k = len F as Element of NAT ;

A1: k = len F ;

A2: for k being Nat st S

S

proof

A7:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for F being FinSequence of O st len F = k + 1 holds

Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

hence
SProduct ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

let F be FinSequence of O; :: thesis: ( len F = k + 1 implies Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) )

assume A4: len F = k + 1 ; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

then consider Fk being FinSequence of O, o9 being Element of O such that

A5: F = Fk ^ <*o9*> by FINSEQ_2:19;

len F = (len Fk) + (len <*o9*>) by A5, FINSEQ_1:22;

then A6: k + 1 = (len Fk) + 1 by A4, FINSEQ_1:39;

set F2k = <*o*> ^ Fk;

thus Product ((<*o*> ^ F),A) = Product (((<*o*> ^ Fk) ^ <*o9*>),A) by A5, FINSEQ_1:32

.= (Product ((<*o*> ^ Fk),A)) * (Product (<*o9*>,A)) by Lm26

.= ((Product (<*o*>,A)) * (Product (Fk,A))) * (Product (<*o9*>,A)) by A3, A6

.= (Product (<*o*>,A)) * ((Product (Fk,A)) * (Product (<*o9*>,A))) by RELAT_1:36

.= (Product (<*o*>,A)) * (Product (F,A)) by A5, Lm26 ; :: thesis: verum

end;assume A4: len F = k + 1 ; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

then consider Fk being FinSequence of O, o9 being Element of O such that

A5: F = Fk ^ <*o9*> by FINSEQ_2:19;

len F = (len Fk) + (len <*o9*>) by A5, FINSEQ_1:22;

then A6: k + 1 = (len Fk) + 1 by A4, FINSEQ_1:39;

set F2k = <*o*> ^ Fk;

thus Product ((<*o*> ^ F),A) = Product (((<*o*> ^ Fk) ^ <*o9*>),A) by A5, FINSEQ_1:32

.= (Product ((<*o*> ^ Fk),A)) * (Product (<*o9*>,A)) by Lm26

.= ((Product (<*o*>,A)) * (Product (Fk,A))) * (Product (<*o9*>,A)) by A3, A6

.= (Product (<*o*>,A)) * ((Product (Fk,A)) * (Product (<*o9*>,A))) by RELAT_1:36

.= (Product (<*o*>,A)) * (Product (F,A)) by A5, Lm26 ; :: thesis: verum

proof

for k being Nat holds S
let F be FinSequence of O; :: thesis: ( len F = 0 implies Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) )

assume A8: len F = 0 ; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

then F = <*> O ;

hence Product ((<*o*> ^ F),A) = Product (<*o*>,A) by FINSEQ_1:34

.= (Product (<*o*>,A)) * (id E) by FUNCT_2:17

.= (Product (<*o*>,A)) * (Product (F,A)) by A8, Def3 ;

:: thesis: verum

end;assume A8: len F = 0 ; :: thesis: Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

then F = <*> O ;

hence Product ((<*o*> ^ F),A) = Product (<*o*>,A) by FINSEQ_1:34

.= (Product (<*o*>,A)) * (id E) by FUNCT_2:17

.= (Product (<*o*>,A)) * (Product (F,A)) by A8, Def3 ;

:: thesis: verum

hence Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) by A1; :: thesis: verum