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:45
.= (F [:] (p ^ q),d9) ^ <*(F . d,d9)*> by Th15
.= (F [:] p,d9) ^ ((F [:] q,d9) ^ <*(F . d,d9)*>) by A2, FINSEQ_1:45
.= (F [:] p,d9) ^ (F [:] (q ^ <*d*>),d9) by Th15 ; :: thesis: verum

end;

F [:] (p ^ (<*> D)),d9 = F [:] p,d9 by FINSEQ_1:47
.= (F [:] p,d9) ^ (<*> E) by FINSEQ_1:47
.= (F [:] p,d9) ^ (F [:] (<*> D),d9) by FINSEQ_2:99 ;
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