let D, D9, E 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:32
.= (F [;] (d,(p9 ^ q9))) ^ <*(F . (d,d9))*> by Th12
.= (F [;] (d,p9)) ^ ((F [;] (d,q9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32
.= (F [;] (d,p9)) ^ (F [;] (d,(q9 ^ <*d9*>))) by Th12 ; :: thesis: verum

end;

F [;] (d,(p9 ^ (<*> D9))) = F [;] (d,p9) by FINSEQ_1:34
.= (F [;] (d,p9)) ^ (<*> E) by FINSEQ_1:34
.= (F [;] (d,p9)) ^ (F [;] (d,(<*> D9))) by FINSEQ_2:79 ;
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