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_{1}[ 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_{1}[k] holds

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

hence Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by A1; :: thesis: verum

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

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

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 F1, F2 being FinSequence of O st len F1 = k + 1 holds

Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))

hence
SProduct ((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;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

proof

for k being Nat holds S
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;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

hence Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by A1; :: thesis: verum