let O be non empty set ; :: thesis: for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
let E be set ; :: thesis: for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
let F1, F2 be FinSequence of O; :: thesis: for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
let A be Action of O,E; :: thesis: Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
defpred S₁[ Nat] means for F1, F2 being FinSequence of O st len F1 = $1 holds
Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A));
reconsider k = len F1 as Element of NAT ;
A1: k = len F1 ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

now :: thesis: for F1, F2 being FinSequence of O st len F1 = k + 1 holds
Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))

let F1, F2 be FinSequence of O; :: thesis: ( len F1 = k + 1 implies Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) )
assume A4: len F1 = k + 1 ; :: thesis: Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
then consider F1k being FinSequence of O, o being Element of O such that
A5: F1 = F1k ^ <*o*> by FINSEQ_2:19;
set F2k = <*o*> ^ F2;
len F1 = (len F1k) + (len <*o*>) by A5, FINSEQ_1:22;
then A6: k + 1 = (len F1k) + 1 by A4, FINSEQ_1:39;
thus Product ((F1 ^ F2),A) = Product ((F1k ^ (<*o*> ^ F2)),A) by A5, FINSEQ_1:32
.= (Product (F1k,A)) * (Product ((<*o*> ^ F2),A)) by A3, A6
.= (Product (F1k,A)) * ((Product (<*o*>,A)) * (Product (F2,A))) by Lm27
.= ((Product (F1k,A)) * (Product (<*o*>,A))) * (Product (F2,A)) by RELAT_1:36
.= (Product (F1,A)) * (Product (F2,A)) by A3, A5, A6 ; :: thesis: verum

end;

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

end;

A7: S₁[ 0 ]

proof

let F1, F2 be FinSequence of O; :: thesis: ( len F1 = 0 implies Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) )
assume A8: len F1 = 0 ; :: thesis: Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))
then F1 = <*> O ;
hence Product ((F1 ^ F2),A) = Product (F2,A) by FINSEQ_1:34
.= (id E) * (Product (F2,A)) by FUNCT_2:17
.= (Product (F1,A)) * (Product (F2,A)) by A8, Def3 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A2);
hence Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by A1; :: thesis: verum