let D9, E, D 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₁[ 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₁[q] holds
S₁[q ^ <*d*>]

proof

let q be FinSequence of D; :: thesis: for d being Element of D st S₁[q] holds
S₁[q ^ <*d*>]
let d be Element of D; :: thesis: ( S₁[q] implies S₁[q ^ <*d*>] )
assume A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: S₁[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 Th15
.= (F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32
.= (F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9)) by Th15 ; :: thesis: verum

end;

F [:] ((p ^ (<*> D)),d9) = F [:] (p,d9) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (<*> E) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (F [:] ((<*> D),d9)) by FINSEQ_2:85 ;
then A3: S₁[ <*> D] ;
for q being FinSequence of D holds S₁[q] from FINSEQ_2:sch 2(A3, A1);
hence F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: verum