let D, E, D9 be non empty set ; :: thesis: for d being Element of D
for F being Function of [:D,D9:],E
for p9, q9 being FinSequence of D9 holds F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9)
let d be Element of D; :: thesis: for F being Function of [:D,D9:],E
for p9, q9 being FinSequence of D9 holds F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9)
let F be Function of [:D,D9:],E; :: thesis: for p9, q9 being FinSequence of D9 holds F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9)
let p9, q9 be FinSequence of D9; :: thesis: F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9)
defpred S₁[ FinSequence of D9] means F [;] d,(p9 ^ $1) = (F [;] d,p9) ^ (F [;] d,$1);
A1: for q9 being FinSequence of D9
for d9 being Element of D9 st S₁[q9] holds
S₁[q9 ^ <*d9*>]

proof

let q9 be FinSequence of D9; :: thesis: for d9 being Element of D9 st S₁[q9] holds
S₁[q9 ^ <*d9*>]
let d9 be Element of D9; :: thesis: ( S₁[q9] implies S₁[q9 ^ <*d9*>] )
assume A2: F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9) ; :: thesis: S₁[q9 ^ <*d9*>]
thus F [;] d,(p9 ^ (q9 ^ <*d9*>)) = F [;] d,((p9 ^ q9) ^ <*d9*>) by FINSEQ_1:45
.= (F [;] d,(p9 ^ q9)) ^ <*(F . d,d9)*> by Th13
.= (F [;] d,p9) ^ ((F [;] d,q9) ^ <*(F . d,d9)*>) by A2, FINSEQ_1:45
.= (F [;] d,p9) ^ (F [;] d,(q9 ^ <*d9*>)) by Th13 ; :: thesis: verum

end;

F [;] d,(p9 ^ (<*> D9)) = F [;] d,p9 by FINSEQ_1:47
.= (F [;] d,p9) ^ (<*> E) by FINSEQ_1:47
.= (F [;] d,p9) ^ (F [;] d,(<*> D9)) by FINSEQ_2:93 ;
then A3: S₁[ <*> D9] ;
for q9 being FinSequence of D9 holds S₁[q9] from FINSEQ_2:sch 2(A3, A1);
hence F [;] d,(p9 ^ q9) = (F [;] d,p9) ^ (F [;] d,q9) ; :: thesis: verum