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₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now

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:22;
len F = (len Fk) + (len <*o9*>) by A5, FINSEQ_1:35;
then A6: k + 1 = (len Fk) + 1 by A4, FINSEQ_1:56;
set F2k = <*o*> ^ Fk;
thus Product (<*o*> ^ F),A = Product ((<*o*> ^ Fk) ^ <*o9*>),A by A5, FINSEQ_1:45
.= (Product (<*o*> ^ Fk),A) * (Product <*o9*>,A) by Lm27
.= ((Product <*o*>,A) * (Product Fk,A)) * (Product <*o9*>,A) by A3, A6
.= (Product <*o*>,A) * ((Product Fk,A) * (Product <*o9*>,A)) by RELAT_1:55
.= (Product <*o*>,A) * (Product F,A) by A5, Lm27 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A7: S₁[ 0 ]

proof

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*> ^ (<*> O)),A
.= Product <*o*>,A by FINSEQ_1:47
.= (Product <*o*>,A) * (id E) by FUNCT_2:23
.= (Product <*o*>,A) * (Product F,A) by A8, Def3 ;
:: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A2);
hence Product (<*o*> ^ F),A = (Product <*o*>,A) * (Product F,A) by A1; :: thesis: verum