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 S1[ 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 S1[q9] holds
S1[q9 ^ <*d9*>]
proof
let q9 be FinSequence of D9; :: thesis: for d9 being Element of D9 st S1[q9] holds
S1[q9 ^ <*d9*>]

let d9 be Element of D9; :: thesis: ( S1[q9] implies S1[q9 ^ <*d9*>] )
assume A2: F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; :: thesis: S1[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
.= (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: S1[ <*> D9] ;
for q9 being FinSequence of D9 holds S1[q9] from hence F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; :: thesis: verum