let D, D9, E be non empty set ; :: thesis: for d9 being Element of D9

for F being Function of [:D,D9:],E

for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E

for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let F be Function of [:D,D9:],E; :: thesis: for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let p, q be FinSequence of D; :: thesis: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

defpred S_{1}[ FinSequence of D] means F [:] ((p ^ $1),d9) = (F [:] (p,d9)) ^ (F [:] ($1,d9));

A1: for q being FinSequence of D

for d being Element of D st S_{1}[q] holds

S_{1}[q ^ <*d*>]

.= (F [:] (p,d9)) ^ (<*> E) by FINSEQ_1:34

.= (F [:] (p,d9)) ^ (F [:] ((<*> D),d9)) by FINSEQ_2:85 ;

then A3: S_{1}[ <*> D]
;

for q being FinSequence of D holds S_{1}[q]
from FINSEQ_2:sch 2(A3, A1);

hence F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: verum

for F being Function of [:D,D9:],E

for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E

for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let F be Function of [:D,D9:],E; :: thesis: for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let p, q be FinSequence of D; :: thesis: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

defpred S

A1: for q being FinSequence of D

for d being Element of D st S

S

proof

F [:] ((p ^ (<*> D)),d9) =
F [:] (p,d9)
by FINSEQ_1:34
let q be FinSequence of D; :: thesis: for d being Element of D st S_{1}[q] holds

S_{1}[q ^ <*d*>]

let d be Element of D; :: thesis: ( S_{1}[q] implies S_{1}[q ^ <*d*>] )

assume A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: S_{1}[q ^ <*d*>]

thus F [:] ((p ^ (q ^ <*d*>)),d9) = F [:] (((p ^ q) ^ <*d*>),d9) by FINSEQ_1:32

.= (F [:] ((p ^ q),d9)) ^ <*(F . (d,d9))*> by Th14

.= (F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32

.= (F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9)) by Th14 ; :: thesis: verum

end;S

let d be Element of D; :: thesis: ( S

assume A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: S

thus F [:] ((p ^ (q ^ <*d*>)),d9) = F [:] (((p ^ q) ^ <*d*>),d9) by FINSEQ_1:32

.= (F [:] ((p ^ q),d9)) ^ <*(F . (d,d9))*> by Th14

.= (F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32

.= (F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9)) by Th14 ; :: thesis: verum

.= (F [:] (p,d9)) ^ (<*> E) by FINSEQ_1:34

.= (F [:] (p,d9)) ^ (F [:] ((<*> D),d9)) by FINSEQ_2:85 ;

then A3: S

for q being FinSequence of D holds S

hence F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: verum