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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for F being FinSequence of O st len F = k + 1 holds
Product ((<*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 ;
then A6: k + 1 = (len Fk) + 1 by ;
set F2k = <*o*> ^ Fk;
thus Product ((<*o*> ^ F),A) = Product (((<*o*> ^ Fk) ^ <*o9*>),A) by
.= (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 ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A7: S1[ 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*>,A) by FINSEQ_1:34
.= (Product (<*o*>,A)) * (id E) by FUNCT_2:17
.= (Product (<*o*>,A)) * (Product (F,A)) by ;
:: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A7, A2);
hence Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) by A1; :: thesis: verum